-- |
-- Module      :  Cryptol.TypeCheck.Solve
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
module Cryptol.TypeCheck.Solve
  ( simplifyAllConstraints
  , proveImplication
  , tryProveImplication
  , proveModuleTopLevel
  , defaultAndSimplify
  , defaultReplExpr
  ) where

import           Cryptol.Parser.Position(thing,emptyRange)
import           Cryptol.TypeCheck.PP -- (pp)
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.Monad
import           Cryptol.TypeCheck.Default
import           Cryptol.TypeCheck.SimpType(tWidth)
import           Cryptol.TypeCheck.Error(Error(..),Warning(..))
import           Cryptol.TypeCheck.Subst
                    (apSubst, isEmptySubst, substToList,
                          emptySubst,Subst,(@@), Subst, listParamSubst)
import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
import           Cryptol.TypeCheck.Solver.Types
import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)

import           Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,isNumeric)
import           Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
import           Cryptol.TypeCheck.Solver.Numeric.Interval
import           Cryptol.Utils.Patterns(matchMaybe)

import           Control.Applicative ((<|>))
import           Control.Monad(mzero)
import           Data.Containers.ListUtils (nubOrd)
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.List(partition)
import           Data.Maybe(listToMaybe,fromMaybe)





quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst,[Goal]))
quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
quickSolverIO Ctxt
_ [] = Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
emptySubst, []))
quickSolverIO Ctxt
ctxt [Goal]
gs =
  case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
gs of
    Left Error
err -> Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left Error
err)
    Right (Subst
su,[Goal]
gs') ->
      do Doc -> IO ()
forall {m :: * -> *} {p}. Monad m => p -> m ()
msg ([Doc] -> Doc
vcat ((Goal -> Doc) -> [Goal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Doc
forall a. PP a => a -> Doc
pp (Type -> Doc) -> (Goal -> Type) -> Goal -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
su]))
         Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[Goal]
gs'))
  where
  msg :: p -> m ()
msg p
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-
  shAsmps = case [ pp x <+> text "in" <+> ppInterval i |
               (x,i) <- Map.toList ctxt ] of
              [] -> text ""
              xs -> text "ASMPS:" $$ nest 2 (vcat xs $$ text "===")
  msg d = putStrLn $ show (
             text "quickSolver:" $$ nest 2 (vcat
                [ shAsmps
                , vcat (map (pp.goal) gs)
                , text "==>"
                , d
                ])) -- -}

quickSolver :: Ctxt   -- ^ Facts we can know
            -> [Goal] -- ^ Need to solve these
            -> Either Error (Subst,[Goal])
            -- ^ Left: contradicting goals,
            --   Right: inferred types, unsolved goals.
quickSolver :: Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
gs0 = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
emptySubst [] [Goal]
gs0
  where
  go :: Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [] [] = (Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[])

  go Subst
su [Goal]
unsolved [] =
    case Match (Either Error (Subst, [Goal]))
-> Maybe (Either Error (Subst, [Goal]))
forall a. Match a -> Maybe a
matchMaybe (Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement Incompatible
noIncompatible [Goal]
unsolved) of
      Maybe (Either Error (Subst, [Goal]))
Nothing -> (Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[Goal]
unsolved)
      Just Either Error (Subst, [Goal])
imp ->
        case Either Error (Subst, [Goal])
imp of
          Right (Subst
newSu, [Goal]
subs) ->
            Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go (Subst
newSu Subst -> Subst -> Subst
@@ Subst
su) [] ([Goal]
subs [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
newSu [Goal]
unsolved)
          Left Error
err -> Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left Error
err

  go Subst
su [Goal]
unsolved (Goal
g : [Goal]
gs)
    | Type -> Set Type -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Type
goal Goal
g) (Ctxt -> Set Type
saturatedAsmps Ctxt
ctxt) = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [Goal]
unsolved [Goal]
gs

  go Subst
su [Goal]
unsolved (Goal
g : [Goal]
gs) =
    case Ctxt -> Type -> Solved
Simplify.simplifyStep Ctxt
ctxt (Goal -> Type
goal Goal
g) of
      Solved
Unsolvable          -> Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left ([Goal] -> Error
UnsolvableGoals [Goal
g])
      Solved
Unsolved            -> Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su (Goal
g Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
unsolved) [Goal]
gs
      SolvedIf [Type]
subs       ->
        let cvt :: Type -> Goal
cvt Type
x = Goal
g { goal = x }
        in Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [Goal]
unsolved ((Type -> Goal) -> [Type] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Goal
cvt [Type]
subs [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
gs)

  -- Probably better to find more than one.
  findImprovement :: Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement Incompatible
inc [] =
    do let bad :: Map TVar (Goal, Goal)
bad = (Goal -> Goal -> (Goal, Goal))
-> Map TVar Goal -> Map TVar Goal -> Map TVar (Goal, Goal)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) (Incompatible -> Map TVar Goal
integralTVars Incompatible
inc) (Incompatible -> Map TVar Goal
fracTVars Incompatible
inc)
       case Map TVar (Goal, Goal)
-> Maybe ((Goal, Goal), Map TVar (Goal, Goal))
forall k a. Map k a -> Maybe (a, Map k a)
Map.minView Map TVar (Goal, Goal)
bad of
         Just ((Goal
g1,Goal
g2),Map TVar (Goal, Goal)
_) -> Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall a. a -> Match a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Error (Subst, [Goal])
 -> Match (Either Error (Subst, [Goal])))
-> Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall a b. (a -> b) -> a -> b
$ Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left (Error -> Either Error (Subst, [Goal]))
-> Error -> Either Error (Subst, [Goal])
forall a b. (a -> b) -> a -> b
$ [Goal] -> Error
UnsolvableGoals [Goal
g1,Goal
g2]
         Maybe ((Goal, Goal), Map TVar (Goal, Goal))
Nothing -> Match (Either Error (Subst, [Goal]))
forall a. Match a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

  findImprovement Incompatible
inc (Goal
g : [Goal]
gs) =
    do (Subst
su,[Type]
ps) <- Bool -> Ctxt -> Type -> Match (Subst, [Type])
improveProp Bool
False Ctxt
ctxt (Goal -> Type
goal Goal
g)
       Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su, [ Goal
g { goal = p } | Type
p <- [Type]
ps ]))
    Match (Either Error (Subst, [Goal]))
-> Match (Either Error (Subst, [Goal]))
-> Match (Either Error (Subst, [Goal]))
forall a. Match a -> Match a -> Match a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement (Goal -> Incompatible -> Incompatible
addIncompatible Goal
g Incompatible
inc) [Goal]
gs


--------------------------------------------------------------------------------
-- Look for type variable with incompatible constraints

data Incompatible = Incompatible
  { Incompatible -> Map TVar Goal
integralTVars :: Map TVar Goal    -- ^ Integral a
  , Incompatible -> Map TVar Goal
fracTVars     :: Map TVar Goal    -- ^ Field a or FLiteral 
  }

noIncompatible :: Incompatible
noIncompatible :: Incompatible
noIncompatible = Incompatible
  { integralTVars :: Map TVar Goal
integralTVars = Map TVar Goal
forall k a. Map k a
Map.empty
  , fracTVars :: Map TVar Goal
fracTVars     = Map TVar Goal
forall k a. Map k a
Map.empty
  }

addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible Goal
g Incompatible
i =
  Incompatible -> Maybe Incompatible -> Incompatible
forall a. a -> Maybe a -> a
fromMaybe Incompatible
i (Maybe Incompatible -> Incompatible)
-> Maybe Incompatible -> Incompatible
forall a b. (a -> b) -> a -> b
$
  do TVar
tv <- Type -> Maybe TVar
tIsVar (Type -> Maybe TVar) -> Maybe Type -> Maybe TVar
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Maybe Type
pIsIntegral (Goal -> Type
goal Goal
g)
     Incompatible -> Maybe Incompatible
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { integralTVars = Map.insert tv g (integralTVars i) }
  Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  do TVar
tv <- Type -> Maybe TVar
tIsVar (Type -> Maybe TVar) -> Maybe Type -> Maybe TVar
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Maybe Type
pIsField (Goal -> Type
goal Goal
g)
     Incompatible -> Maybe Incompatible
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars = Map.insert tv g (fracTVars i) }
  Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  do (Type
_,Type
_,Type
_,Type
t) <- Type -> Maybe (Type, Type, Type, Type)
pIsFLiteral (Goal -> Type
goal Goal
g)
     TVar
tv        <- Type -> Maybe TVar
tIsVar Type
t
     Incompatible -> Maybe Incompatible
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars = Map.insert tv g (fracTVars i) }





--------------------------------------------------------------------------------


defaultReplExpr :: Solver -> Expr -> Schema ->
                    IO (Maybe ([(TParam,Type)], Expr))

defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
defaultReplExpr Solver
sol Expr
expr Schema
sch =
  do Maybe [(TParam, Type)]
mb <- Solver -> [TParam] -> [Type] -> IO (Maybe [(TParam, Type)])
defaultReplExpr' Solver
sol [TParam]
numVs [Type]
numPs
     case Maybe [(TParam, Type)]
mb of
       Maybe [(TParam, Type)]
Nothing -> Maybe ([(TParam, Type)], Expr)
-> IO (Maybe ([(TParam, Type)], Expr))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(TParam, Type)], Expr)
forall a. Maybe a
Nothing
       Just [(TParam, Type)]
numBinds -> Maybe ([(TParam, Type)], Expr)
-> IO (Maybe ([(TParam, Type)], Expr))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(TParam, Type)], Expr)
 -> IO (Maybe ([(TParam, Type)], Expr)))
-> Maybe ([(TParam, Type)], Expr)
-> IO (Maybe ([(TParam, Type)], Expr))
forall a b. (a -> b) -> a -> b
$
         do let optss :: [[(TParam, Type)]]
optss = (TParam -> [(TParam, Type)]) -> [TParam] -> [[(TParam, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> [(TParam, Type)]
tryDefVar [TParam]
otherVs
            [(TParam, Type)]
su    <- [[(TParam, Type)]] -> Maybe [(TParam, Type)]
forall a. [a] -> Maybe a
listToMaybe
                       [ [(TParam, Type)]
binds | [(TParam, Type)]
nonSu <- [[(TParam, Type)]] -> [[(TParam, Type)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [[(TParam, Type)]]
optss
                               , let binds :: [(TParam, Type)]
binds = [(TParam, Type)]
nonSu [(TParam, Type)] -> [(TParam, Type)] -> [(TParam, Type)]
forall a. [a] -> [a] -> [a]
++ [(TParam, Type)]
numBinds
                               , [(TParam, Type)] -> Bool
validate [(TParam, Type)]
binds ]
            [Type]
tys <- [Maybe Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ TParam -> [(TParam, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TParam
v [(TParam, Type)]
su | TParam
v <- Schema -> [TParam]
sVars Schema
sch ]
            ([(TParam, Type)], Expr) -> Maybe ([(TParam, Type)], Expr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Type)]
su, [Type] -> Expr
forall {t :: * -> *}. Foldable t => t Type -> Expr
appExpr [Type]
tys)

  where
  validate :: [(TParam, Type)] -> Bool
validate [(TParam, Type)]
binds =
    let su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
binds
    in [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Schema -> [Type]
sProps Schema
sch)))

  ([TParam]
numVs,[TParam]
otherVs) = (TParam -> Bool) -> [TParam] -> ([TParam], [TParam])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Kind -> TParam -> Bool
forall {t}. HasKind t => Kind -> t -> Bool
kindIs Kind
KNum) (Schema -> [TParam]
sVars Schema
sch)
  ([Type]
numPs,[Type]
otherPs) = (Type -> Bool) -> [Type] -> ([Type], [Type])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Type -> Bool
isNumeric (Schema -> [Type]
sProps Schema
sch)


  kindIs :: Kind -> t -> Bool
kindIs Kind
k t
x = t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k

  gSet :: Goals
gSet  = [Goal] -> Goals
goalsFromList
           [ Goal { goal :: Type
goal = Type
p
                  , goalRange :: Range
goalRange = Range
emptyRange
                  , goalSource :: ConstraintSource
goalSource = ConstraintSource
CtDefaulting } | Type
p <- [Type]
otherPs ]

  fLitGoals :: Map TVar (Maybe ((TVar, Type), Warning))
fLitGoals = Goals -> Map TVar (Maybe ((TVar, Type), Warning))
flitDefaultCandidates Goals
gSet

  tryDefVar :: TParam -> [(TParam, Type)]
  tryDefVar :: TParam -> [(TParam, Type)]
tryDefVar TParam
a
    -- REPL defaulting for floating-point literals
    | Just Maybe ((TVar, Type), Warning)
m <- TVar
-> Map TVar (Maybe ((TVar, Type), Warning))
-> Maybe (Maybe ((TVar, Type), Warning))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (TParam -> TVar
TVBound TParam
a) Map TVar (Maybe ((TVar, Type), Warning))
fLitGoals
    = case Maybe ((TVar, Type), Warning)
m of
        Just ((TVar
_,Type
t),Warning
_) -> [(TParam
a,Type
t)]
        Maybe ((TVar, Type), Warning)
Nothing        -> []

    -- REPL defaulting for integer literals
    | Just Goal
gt <- TVar -> Map TVar Goal -> Maybe Goal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (TParam -> TVar
TVBound TParam
a) (Goals -> Map TVar Goal
literalGoals Goals
gSet)
    = let ok :: t -> Bool
ok t
p = Bool -> Bool
not (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (TParam -> TVar
TVBound TParam
a) (t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs t
p)) in
      [ (TParam
a,Type
t) | Type
t <- [ Type
tInteger, Type -> Type
tWord (Type -> Type
tWidth (Goal -> Type
goal Goal
gt)) ]
              , Type -> Bool
forall {t}. FVS t => t -> Bool
ok Type
t ]

    -- REPL defaulting for variables unconstrained by a literal constraint
    | Bool
otherwise = [ (TParam
a,Type
t) | Type
t <- [Type
tInteger, Type
tRational, Type
tBit] ]

  appExpr :: t Type -> Expr
appExpr t Type
tys = (Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e1 Type
_ -> Expr -> Expr
EProofApp Expr
e1)
                      ((Expr -> Type -> Expr) -> Expr -> t Type -> Expr
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
ETApp Expr
expr t Type
tys)
                      (Schema -> [Type]
sProps Schema
sch)


defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning],[Error])
defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
as [Goal]
gs =
  let ([TVar]
as1, [Goal]
gs1, Subst
su1, [Warning]
ws) = ([TVar], [Goal], Subst, [Warning])
defLit
      ([TVar]
as2, [Goal]
gs2, Subst
su2, [Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
improveByDefaultingWithPure [TVar]
as1 [Goal]
gs1
  in ([TVar]
as2,[Goal]
gs2,Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Warning]
ws, [Error]
errs)

  where
  defLit :: ([TVar], [Goal], Subst, [Warning])
defLit
    | Subst -> Bool
isEmptySubst Subst
su = ([TVar], [Goal], Subst, [Warning])
forall {a}. ([TVar], [Goal], Subst, [a])
nope
    | Bool
otherwise       = case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
forall a. Monoid a => a
mempty (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs) of
                          Left Error
_ -> ([TVar], [Goal], Subst, [Warning])
forall {a}. ([TVar], [Goal], Subst, [a])
nope -- hm?
                          Right (Subst
su1,[Goal]
gs1) -> ([TVar]
as1,[Goal]
gs1,Subst
su1Subst -> Subst -> Subst
@@Subst
su,[Warning]
ws)
    where ([TVar]
as1,Subst
su,[Warning]
ws) = [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals [TVar]
as [Goal]
gs
          nope :: ([TVar], [Goal], Subst, [a])
nope        = ([TVar]
as,[Goal]
gs,Subst
emptySubst,[])



simplifyAllConstraints :: InferM ()
simplifyAllConstraints :: InferM ()
simplifyAllConstraints =
  do InferM ()
simpHasGoals
     [Goal]
gs <- InferM [Goal]
getGoals
     case [Goal]
gs of
       [] -> () -> InferM ()
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [Goal]
_ ->
        case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
forall a. Monoid a => a
mempty [Goal]
gs of
          Left Error
err -> Error -> InferM ()
recordError Error
err
          Right (Subst
su,[Goal]
gs1) ->
            do Subst -> InferM ()
extendSubst Subst
su
               [Goal] -> InferM ()
addGoals [Goal]
gs1

-- | Simplify @Has@ constraints as much as possible.
simpHasGoals :: InferM ()
simpHasGoals :: InferM ()
simpHasGoals = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] ([HasGoal] -> InferM ()) -> InferM [HasGoal] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InferM [HasGoal]
getHasGoals
  where
  go :: Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
_     []       []  = () -> InferM ()
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  go Bool
True  [HasGoal]
unsolved []  = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] [HasGoal]
unsolved
  go Bool
False [HasGoal]
unsolved []  = (HasGoal -> InferM ()) -> [HasGoal] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ HasGoal -> InferM ()
addHasGoal [HasGoal]
unsolved

  go Bool
changes [HasGoal]
unsolved (HasGoal
g : [HasGoal]
todo) =
    do (Bool
ch,Bool
solved) <- HasGoal -> InferM (Bool, Bool)
tryHasGoal HasGoal
g
       let changes' :: Bool
changes'  = Bool
ch Bool -> Bool -> Bool
|| Bool
changes
           unsolved' :: [HasGoal]
unsolved' = if Bool
solved then [HasGoal]
unsolved else HasGoal
g HasGoal -> [HasGoal] -> [HasGoal]
forall a. a -> [a] -> [a]
: [HasGoal]
unsolved
       Bool
changes' Bool -> InferM () -> InferM ()
forall a b. a -> b -> b
`seq` [HasGoal]
unsolved [HasGoal] -> InferM () -> InferM ()
forall a b. a -> b -> b
`seq` Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
changes' [HasGoal]
unsolved' [HasGoal]
todo


-- | Try to clean-up any left-over constraints after we've checked everything
-- in a module.  Typically these are either trivial things, or constraints
-- on the module's type parameters.
proveModuleTopLevel :: InferM ()
proveModuleTopLevel :: InferM ()
proveModuleTopLevel =
  do InferM ()
simplifyAllConstraints
     [Goal]
gs <- InferM [Goal]
getGoals
     let vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList ((TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV ([Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
gs))
         ([TVar]
_,[Goal]
gs1,Subst
su1,[Warning]
ws,[Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
vs [Goal]
gs
     Subst -> InferM ()
extendSubst Subst
su1
     (Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
     (Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs

     [Located Type]
cs <- InferM [Located Type]
getParamConstraints
     case [Located Type]
cs of
       [] -> [Goal] -> InferM ()
addGoals [Goal]
gs1
       [Located Type]
_  -> do Subst
su2 <- Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication Bool
False Maybe Name
forall a. Maybe a
Nothing [] [] [Goal]
gs1
                Subst -> InferM ()
extendSubst Subst
su2

-- | Prove an implication, and return any improvements that we computed.
-- Records errors, if any of the goals couldn't be solved.
proveImplication :: Bool -> Maybe Name ->
  [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication :: Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication Bool
dedupErrs Maybe Name
lnam [TParam]
as [Type]
ps [Goal]
gs =
  do Set TVar
evars <- InferM (Set TVar)
varsWithAsmps
     Solver
solver <- InferM Solver
getSolver

     [TParam]
extraAs <- ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam ([ModTParam] -> [TParam])
-> (Map Name ModTParam -> [ModTParam])
-> Map Name ModTParam
-> [TParam]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems) (Map Name ModTParam -> [TParam])
-> InferM (Map Name ModTParam) -> InferM [TParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
     [Type]
extra   <- (Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing ([Located Type] -> [Type])
-> InferM [Located Type] -> InferM [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM [Located Type]
getParamConstraints

     (Either [Error] [Warning]
mbErr,Subst
su) <- IO (Either [Error] [Warning], Subst)
-> InferM (Either [Error] [Warning], Subst)
forall a. IO a -> InferM a
io (Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
solver Bool
dedupErrs Maybe Name
lnam Set TVar
evars
                            ([TParam]
extraAs [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ [TParam]
as) ([Type]
extra [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ps) [Goal]
gs)
     case Either [Error] [Warning]
mbErr of
       Right [Warning]
ws  -> (Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
       Left [Error]
errs -> (Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
     Subst -> InferM Subst
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su

-- | Tries to prove an implication. If proved, then returns
-- a (possibly-empty) list of warnings raised during proving.
-- If not proved, then returns `Left errs`, which records all errors
-- raised during proving.
tryProveImplication :: 
  Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM (Either [Error] [Warning])
tryProveImplication :: Maybe Name
-> [TParam]
-> [Type]
-> [Goal]
-> InferM (Either [Error] [Warning])
tryProveImplication Maybe Name
lnam [TParam]
as [Type]
ps [Goal]
gs =
  do Set TVar
evars <- InferM (Set TVar)
varsWithAsmps
     Solver
solver <- InferM Solver
getSolver

     [TParam]
extraAs <- ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam ([ModTParam] -> [TParam])
-> (Map Name ModTParam -> [ModTParam])
-> Map Name ModTParam
-> [TParam]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems) (Map Name ModTParam -> [TParam])
-> InferM (Map Name ModTParam) -> InferM [TParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
     [Type]
extra   <- (Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing ([Located Type] -> [Type])
-> InferM [Located Type] -> InferM [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM [Located Type]
getParamConstraints

     (Either [Error] [Warning]
res,Subst
_su) <- IO (Either [Error] [Warning], Subst)
-> InferM (Either [Error] [Warning], Subst)
forall a. IO a -> InferM a
io (Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
solver Bool
False Maybe Name
lnam Set TVar
evars
                            ([TParam]
extraAs [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ [TParam]
as) ([Type]
extra [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ps) [Goal]
gs)
     Either [Error] [Warning] -> InferM (Either [Error] [Warning])
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Either [Error] [Warning]
res


proveImplicationIO :: Solver
                   -> Bool     -- ^ Whether to remove duplicate goals in errors
                   -> Maybe Name     -- ^ Checking this function
                   -> Set TVar -- ^ These appear in the env., and we should
                               -- not try to default them
                   -> [TParam] -- ^ Type parameters
                   -> [Prop]   -- ^ Assumed constraint
                   -> [Goal]   -- ^ Collected constraints
                   -> IO (Either [Error] [Warning], Subst)
proveImplicationIO :: Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
_ Bool
_         Maybe Name
_ Set TVar
_         [TParam]
_  []     []  = (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
emptySubst)
proveImplicationIO Solver
s Bool
dedupErrs Maybe Name
f Set TVar
varsInEnv [TParam]
ps [Type]
asmps0 [Goal]
gs0 =
  do let ctxt :: Ctxt
ctxt = [Type] -> Ctxt
buildSolverCtxt [Type]
asmps
     Either Error (Subst, [Goal])
res <- Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
quickSolverIO Ctxt
ctxt [Goal]
gs
     case Either Error (Subst, [Goal])
res of
       Left Error
erro -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left [Error
erro], Subst
emptySubst)
       Right (Subst
su,[]) -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
su)
       Right (Subst
su,[Goal]
gs1) ->
         do [Goal]
gs2 <- Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp Solver
s [Type]
asmps [Goal]
gs1
            case [Goal]
gs2 of
              [] -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
su)
              [Goal]
gs3 ->
                do let free :: [TVar]
free = (TVar -> Bool) -> [TVar] -> [TVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TVar -> Bool
isFreeTV
                            ([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList
                            (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([Type] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ((Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs3)) Set TVar
varsInEnv
                   case [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
free [Goal]
gs3 of
                     ([TVar]
_,[Goal]
_,Subst
newSu,[Warning]
_,[Error]
errs)
                        | Subst -> Bool
isEmptySubst Subst
newSu ->
                                 (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left ([Goal] -> Error
err [Goal]
gs3Error -> [Error] -> [Error]
forall a. a -> [a] -> [a]
:[Error]
errs), Subst
su) -- XXX: Old?
                     ([TVar]
_,[Goal]
newGs,Subst
newSu,[Warning]
ws,[Error]
errs) ->
                       do let su1 :: Subst
su1 = Subst
newSu Subst -> Subst -> Subst
@@ Subst
su
                          (Either [Error] [Warning]
res1,Subst
su2) <- Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
s Bool
dedupErrs Maybe Name
f Set TVar
varsInEnv [TParam]
ps
                                                 (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
asmps0) [Goal]
newGs
                          let su3 :: Subst
su3 = Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1
                          case Either [Error] [Warning]
res1 of
                            Left [Error]
bad -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left ([Error]
bad [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ [Error]
errs), Subst
su3)
                            Right [Warning]
ws1
                              | [Error] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Error]
errs -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right ([Warning]
ws[Warning] -> [Warning] -> [Warning]
forall a. [a] -> [a] -> [a]
++[Warning]
ws1),Subst
su3)
                              | Bool
otherwise -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left [Error]
errs, Subst
su3)
  where
  err :: [Goal] -> Error
err [Goal]
us = Error -> Error
cleanupError
           (Error -> Error) -> Error -> Error
forall a b. (a -> b) -> a -> b
$ DelayedCt -> Error
UnsolvedDelayedCt
           (DelayedCt -> Error) -> DelayedCt -> Error
forall a b. (a -> b) -> a -> b
$ DelayedCt { dctSource :: Maybe Name
dctSource = Maybe Name
f
                       , dctForall :: [TParam]
dctForall = [TParam]
ps
                       , dctAsmps :: [Type]
dctAsmps  = [Type]
asmps0
                       , dctGoals :: [Goal]
dctGoals  = if Bool
dedupErrs then [Goal] -> [Goal]
forall a. Ord a => [a] -> [a]
nubOrd [Goal]
us else [Goal]
us
                       }


  asmps1 :: [Type]
asmps1 = (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
asmps0
  ([Type]
asmps,[Goal]
gs) =
     let gs1 :: [Goal]
gs1 = [ Goal
g { goal = p } | Goal
g <- [Goal]
gs0, Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g)
                                , Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Type
p [Type]
asmps1 ]
     in case Match (Subst, [Type]) -> Maybe (Subst, [Type])
forall a. Match a -> Maybe a
matchMaybe (Bool -> Ctxt -> [Type] -> Match (Subst, [Type])
improveProps Bool
True Ctxt
forall a. Monoid a => a
mempty [Type]
asmps1) of
          Maybe (Subst, [Type])
Nothing -> ([Type]
asmps1,[Goal]
gs1)
          Just (Subst
newSu,[Type]
newAsmps) ->
             ( [ TVar -> Type
TVar TVar
x Type -> Type -> Type
=#= Type
t | (TVar
x,Type
t) <- Subst -> [(TVar, Type)]
substToList Subst
newSu ]
               [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
newAsmps
             , [ Goal
g { goal = apSubst newSu (goal g) } | Goal
g <- [Goal]
gs1 ]
             )




cleanupError :: Error -> Error
cleanupError :: Error -> Error
cleanupError Error
err =
  case Error
err of
    UnsolvedDelayedCt DelayedCt
d ->
      let noInferVars :: Goal -> Bool
noInferVars = Set TVar -> Bool
forall a. Set a -> Bool
Set.null (Set TVar -> Bool) -> (Goal -> Set TVar) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> (Goal -> Set TVar) -> Goal -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type -> Set TVar) -> (Goal -> Type) -> Goal -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal
          without :: [Goal]
without = (Goal -> Bool) -> [Goal] -> [Goal]
forall a. (a -> Bool) -> [a] -> [a]
filter Goal -> Bool
noInferVars (DelayedCt -> [Goal]
dctGoals DelayedCt
d)
      in DelayedCt -> Error
UnsolvedDelayedCt (DelayedCt -> Error) -> DelayedCt -> Error
forall a b. (a -> b) -> a -> b
$
            if Bool -> Bool
not ([Goal] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Goal]
without) then DelayedCt
d { dctGoals = without } else DelayedCt
d

    Error
_ -> Error
err



buildSolverCtxt :: [Prop] -> Ctxt
buildSolverCtxt :: [Type] -> Ctxt
buildSolverCtxt [Type]
ps0 =
  let ps :: Set Type
ps = Set Type -> [Type] -> Set Type
saturateProps Set Type
forall a. Monoid a => a
mempty [Type]
ps0
      ivals :: Map TVar Interval
ivals = Map TVar Interval -> [Type] -> Map TVar Interval
assumptionIntervals Map TVar Interval
forall a. Monoid a => a
mempty (Set Type -> [Type]
forall a. Set a -> [a]
Set.toList Set Type
ps)
   in SolverCtxt
      { intervals :: Map TVar Interval
intervals = Map TVar Interval
ivals
      , saturatedAsmps :: Set Type
saturatedAsmps = Set Type
ps
      }

 where
 saturateProps :: Set Type -> [Type] -> Set Type
saturateProps Set Type
gs [] = Set Type
gs
 saturateProps Set Type
gs (Type
p:[Type]
ps)
   | Type -> Set Type -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Type
p Set Type
gs = Set Type -> [Type] -> Set Type
saturateProps Set Type
gs [Type]
ps
   | Just (Type
n,Type
_) <- Type -> Maybe (Type, Type)
pIsLiteral Type
p =
       let gs' :: Set Type
gs' = [Type] -> Set Type
forall a. Ord a => [a] -> Set a
Set.fromList [Type
p, Type -> Type
pFin Type
n] Set Type -> Set Type -> Set Type
forall a. Semigroup a => a -> a -> a
<> Set Type
gs
        in Set Type -> [Type] -> Set Type
saturateProps Set Type
gs' [Type]
ps
   | Bool
otherwise =
        let gs' :: Set Type
gs' = Type -> Set Type
forall a. a -> Set a
Set.singleton Type
p Set Type -> Set Type -> Set Type
forall a. Semigroup a => a -> a -> a
<> Type -> Set Type
superclassSet Type
p Set Type -> Set Type -> Set Type
forall a. Semigroup a => a -> a -> a
<> Set Type
gs
         in Set Type -> [Type] -> Set Type
saturateProps Set Type
gs' [Type]
ps

 assumptionIntervals :: Map TVar Interval -> [Type] -> Map TVar Interval
assumptionIntervals Map TVar Interval
as [Type]
ps =
   case Map TVar Interval -> [Type] -> IntervalUpdate
computePropIntervals Map TVar Interval
as [Type]
ps of
     IntervalUpdate
NoChange -> Map TVar Interval
as
     InvalidInterval {} -> Map TVar Interval
as -- XXX: say something
     NewIntervals Map TVar Interval
bs -> Map TVar Interval -> Map TVar Interval -> Map TVar Interval
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVar Interval
bs Map TVar Interval
as