{-# LANGUAGE LambdaCase #-}
module Intensional.InferCoreExpr
( inferProg,
)
where
import Intensional.Ubiq
import Control.Monad.Extra
import Control.Monad.RWS.Strict
import Control.Monad.State.Strict as State
import CoreArity
import qualified CoreSyn as Core
import Data.Bifunctor
import qualified Data.IntSet as I
import qualified Data.List as L
import qualified Data.Map as M
import Intensional.FromCore
import GhcPlugins hiding ((<>), Type)
import Intensional.InferM
import Pair
import Intensional.Scheme as Scheme
import Intensional.Guard as Guard
import Intensional.Types
import qualified Intensional.Constraints as Constraints
import Debug.Trace
type SubTyAtom = (Guard, RVar, RVar, TyCon)
type SubTyFrontierAtom = (Guard, RVar, RVar, TyCon, [Type], [Type])
type SubTyComputation = StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
inferSubType :: Type -> Type -> InferM ()
inferSubType :: Type -> Type -> InferM ()
inferSubType t1 :: Type
t1 t2 :: Type
t2 =
do let ts :: [(RVar, RVar, TyCon, [Type], [Type])]
ts = Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep Type
t1 Type
t2
(_,cs :: ConstraintSetF Atomic
cs) <- InferM () -> InferM ((), ConstraintSetF Atomic)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (InferM () -> InferM ((), ConstraintSetF Atomic))
-> InferM () -> InferM ((), ConstraintSetF Atomic)
forall a b. (a -> b) -> a -> b
$
[(RVar, RVar, TyCon, [Type], [Type])]
-> ((RVar, RVar, TyCon, [Type], [Type]) -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(RVar, RVar, TyCon, [Type], [Type])]
ts (((RVar, RVar, TyCon, [Type], [Type]) -> InferM ()) -> InferM ())
-> ((RVar, RVar, TyCon, [Type], [Type]) -> InferM ()) -> InferM ()
forall a b. (a -> b) -> a -> b
$ \(x :: RVar
x, y :: RVar
y, d :: TyCon
d, as :: [Type]
as, as' :: [Type]
as') ->
do
[SubTyAtom]
ds <- ([SubTyFrontierAtom], [SubTyAtom]) -> [SubTyAtom]
forall a b. (a, b) -> b
snd (([SubTyFrontierAtom], [SubTyAtom]) -> [SubTyAtom])
-> InferM ([SubTyFrontierAtom], [SubTyAtom]) -> InferM [SubTyAtom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> ([SubTyFrontierAtom], [SubTyAtom])
-> InferM ([SubTyFrontierAtom], [SubTyAtom])
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
State.execStateT StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
inferSubTypeFix ([(Guard
forall a. Monoid a => a
mempty, RVar
x, RVar
y, TyCon
d, [Type]
as, [Type]
as')],[(Guard
forall a. Monoid a => a
mempty, RVar
x, RVar
y, TyCon
d)])
RVar -> InferM ()
noteD (RVar -> InferM ()) -> RVar -> InferM ()
forall a b. (a -> b) -> a -> b
$ [Name] -> RVar
forall (t :: * -> *) a. Foldable t => t a -> RVar
length ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (SubTyAtom -> Name) -> [SubTyAtom] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\(_,_,_,d' :: TyCon
d') -> TyCon -> Name
forall a. NamedThing a => a -> Name
getName TyCon
d') [SubTyAtom]
ds)
[SubTyAtom] -> (SubTyAtom -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SubTyAtom]
ds ((SubTyAtom -> InferM ()) -> InferM ())
-> (SubTyAtom -> InferM ()) -> InferM ()
forall a b. (a -> b) -> a -> b
$ \(gs :: Guard
gs, x' :: RVar
x', y' :: RVar
y', d' :: TyCon
d') ->
(ConstraintSetF Atomic -> ConstraintSetF Atomic)
-> InferM () -> InferM ()
forall w (m :: * -> *) a. MonadWriter w m => (w -> w) -> m a -> m a
censor (Guard -> ConstraintSetF Atomic -> ConstraintSetF Atomic
Constraints.guardWith Guard
gs) (DataType TyCon -> DataType TyCon -> InferM ()
emitDD (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x' TyCon
d') (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
y' TyCon
d'))
Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugging (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
do SrcSpan
src <- (InferEnv -> SrcSpan)
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity SrcSpan
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> SrcSpan
inferLoc
String -> InferM ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("[TRACE] Starting subtpe inference at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SrcSpan -> String
traceSpan SrcSpan
src)
let sz :: RVar
sz = ConstraintSetF Atomic -> RVar
Constraints.size ConstraintSetF Atomic
cs
String -> InferM ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("[TRACE] The subtype proof at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SrcSpan -> String
traceSpan SrcSpan
src String -> String -> String
forall a. [a] -> [a] -> [a]
++ " contributed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RVar -> String
forall a. Show a => a -> String
show RVar
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " constraints.")
where
leq :: SubTyAtom -> SubTyAtom -> Bool
leq :: SubTyAtom -> SubTyAtom -> Bool
leq (gs :: Guard
gs, x :: RVar
x, y :: RVar
y, d :: TyCon
d) (gs' :: Guard
gs', x' :: RVar
x', y' :: RVar
y', d' :: TyCon
d') =
RVar
x RVar -> RVar -> Bool
forall a. Eq a => a -> a -> Bool
== RVar
x' Bool -> Bool -> Bool
&& RVar
y RVar -> RVar -> Bool
forall a. Eq a => a -> a -> Bool
== RVar
y' Bool -> Bool -> Bool
&& TyCon -> Name
forall a. NamedThing a => a -> Name
getName TyCon
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon -> Name
forall a. NamedThing a => a -> Name
getName TyCon
d' Bool -> Bool -> Bool
&& Guard
gs' Guard -> Guard -> Bool
`Guard.impliedBy` Guard
gs
inferSubTypeFix :: SubTyComputation
inferSubTypeFix :: StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
inferSubTypeFix =
do (frontier :: [SubTyFrontierAtom]
frontier, acc :: [SubTyAtom]
acc) <-StateT
([SubTyFrontierAtom], [SubTyAtom])
InferM
([SubTyFrontierAtom], [SubTyAtom])
forall s (m :: * -> *). MonadState s m => m s
get
Bool
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SubTyFrontierAtom] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SubTyFrontierAtom]
frontier) (StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$
do ([SubTyFrontierAtom], [SubTyAtom])
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([], [SubTyAtom]
acc)
[SubTyFrontierAtom]
-> (SubTyFrontierAtom
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SubTyFrontierAtom]
frontier ((SubTyFrontierAtom
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> (SubTyFrontierAtom
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$ \(gs :: Guard
gs, x :: RVar
x, y :: RVar
y, d :: TyCon
d, as :: [Type]
as, as' :: [Type]
as') ->
do let dataCons :: [DataCon]
dataCons = TyCon -> [DataCon]
tyConDataCons TyCon
d
InferM () -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (InferM () -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> InferM () -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$ RVar -> InferM ()
noteK ([DataCon] -> RVar
forall (t :: * -> *) a. Foldable t => t a -> RVar
length [DataCon]
dataCons)
[DataCon]
-> (DataCon -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [DataCon]
dataCons ((DataCon -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> (DataCon -> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$ \k :: DataCon
k ->
do [Type]
xtys <- RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type])
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type]
forall a b. (a -> b) -> a -> b
$ RVar
-> [Type]
-> DataCon
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
consInstArgs RVar
x [Type]
as DataCon
k
[Type]
ytys <- RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type])
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM [Type]
forall a b. (a -> b) -> a -> b
$ RVar
-> [Type]
-> DataCon
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
consInstArgs RVar
y [Type]
as' DataCon
k
let gs' :: Guard
gs' =
if (TyCon -> Bool
isTrivial TyCon
d)
then Guard
gs
else [Name] -> RVar -> Name -> Guard
Guard.singleton [DataCon -> Name
forall a. NamedThing a => a -> Name
getName DataCon
k] RVar
x (TyCon -> Name
forall a. NamedThing a => a -> Name
getName TyCon
d) Guard -> Guard -> Guard
forall a. Semigroup a => a -> a -> a
<> Guard
gs
let ts :: [(RVar, RVar, TyCon, [Type], [Type])]
ts = [[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])])
-> [[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])])
-> [Type] -> [Type] -> [[(RVar, RVar, TyCon, [Type], [Type])]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep [Type]
xtys [Type]
ytys
[(RVar, RVar, TyCon, [Type], [Type])]
-> ((RVar, RVar, TyCon, [Type], [Type])
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(RVar, RVar, TyCon, [Type], [Type])]
ts (((RVar, RVar, TyCon, [Type], [Type])
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> ((RVar, RVar, TyCon, [Type], [Type])
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$ \(x' :: RVar
x', y' :: RVar
y', d' :: TyCon
d', bs :: [Type]
bs, bs' :: [Type]
bs') ->
do let new :: SubTyAtom
new = (Guard
gs', RVar
x', RVar
y', TyCon
d')
let newF :: SubTyFrontierAtom
newF = (Guard
gs', RVar
x', RVar
y', TyCon
d', [Type]
bs, [Type]
bs')
(fr :: [SubTyFrontierAtom]
fr, ac :: [SubTyAtom]
ac) <- StateT
([SubTyFrontierAtom], [SubTyAtom])
InferM
([SubTyFrontierAtom], [SubTyAtom])
forall s (m :: * -> *). MonadState s m => m s
get
Bool
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((SubTyAtom -> Bool) -> [SubTyAtom] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SubTyAtom -> SubTyAtom -> Bool
`leq` SubTyAtom
new) [SubTyAtom]
ac) (StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ())
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall a b. (a -> b) -> a -> b
$ ([SubTyFrontierAtom], [SubTyAtom])
-> StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (SubTyFrontierAtom
newFSubTyFrontierAtom -> [SubTyFrontierAtom] -> [SubTyFrontierAtom]
forall a. a -> [a] -> [a]
:[SubTyFrontierAtom]
fr, SubTyAtom
newSubTyAtom -> [SubTyAtom] -> [SubTyAtom]
forall a. a -> [a] -> [a]
:[SubTyAtom]
ac)
StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()
inferSubTypeFix
inferSubTypeStep :: Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep :: Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep (Data (Inj x :: RVar
x d :: TyCon
d) as :: [Type]
as) (Data (Inj y :: RVar
y _) as' :: [Type]
as') =
[(RVar
x, RVar
y, TyCon
d, [Type]
as, [Type]
as')]
inferSubTypeStep (t11 :: Type
t11 :=> t12 :: Type
t12) (t21 :: Type
t21 :=> t22 :: Type
t22) =
let ds1 :: [(RVar, RVar, TyCon, [Type], [Type])]
ds1 = Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep Type
t21 Type
t11
ds2 :: [(RVar, RVar, TyCon, [Type], [Type])]
ds2 = Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep Type
t12 Type
t22
in [(RVar, RVar, TyCon, [Type], [Type])]
ds1 [(RVar, RVar, TyCon, [Type], [Type])]
-> [(RVar, RVar, TyCon, [Type], [Type])]
-> [(RVar, RVar, TyCon, [Type], [Type])]
forall a. [a] -> [a] -> [a]
++ [(RVar, RVar, TyCon, [Type], [Type])]
ds2
inferSubTypeStep (Data (Base _) as :: [Type]
as) (Data (Base _) as' :: [Type]
as') =
[[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])])
-> [[(RVar, RVar, TyCon, [Type], [Type])]]
-> [(RVar, RVar, TyCon, [Type], [Type])]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])])
-> [Type] -> [Type] -> [[(RVar, RVar, TyCon, [Type], [Type])]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]
inferSubTypeStep [Type]
as [Type]
as'
inferSubTypeStep _ _ = []
inferProg :: CoreProgram -> InferM Context
inferProg :: CoreProgram -> InferM Context
inferProg [] = Context -> InferM Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
forall k a. Map k a
M.empty
inferProg (r :: CoreBind
r : rs :: CoreProgram
rs) =
do let bs :: [OccName]
bs = (CoreBndr -> OccName) -> [CoreBndr] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map CoreBndr -> OccName
forall name. HasOccName name => name -> OccName
occName ([CoreBndr] -> [OccName]) -> [CoreBndr] -> [OccName]
forall a b. (a -> b) -> a -> b
$ CoreBind -> [CoreBndr]
forall b. Bind b -> [b]
bindersOf CoreBind
r
Context
ctx <- if (OccName -> Bool) -> [OccName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any OccName -> Bool
isDerivedOccName [OccName]
bs then Context -> InferM Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
forall a. Monoid a => a
mempty else CoreBind -> InferM Context
associate CoreBind
r
Context
ctxs <- Context -> InferM Context -> InferM Context
forall a. Context -> InferM a -> InferM a
putVars Context
ctx (CoreProgram -> InferM Context
inferProg CoreProgram
rs)
Context -> InferM Context
forall (m :: * -> *) a. Monad m => a -> m a
return (Context
ctxs Context -> Context -> Context
forall a. Semigroup a => a -> a -> a
<> Context
ctx)
associate :: CoreBind -> InferM Context
associate :: CoreBind -> InferM Context
associate r :: CoreBind
r =
SrcSpan -> InferM Context -> InferM Context
forall a. SrcSpan -> InferM a -> InferM a
setLoc (FastString -> SrcSpan
UnhelpfulSpan (String -> FastString
mkFastString ("Top level " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bindingNames))) InferM Context
doAssoc
where
bindingNames :: String
bindingNames =
[String] -> String
forall a. Show a => a -> String
show ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (CoreBndr -> String) -> [CoreBndr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (OccName -> String
occNameString (OccName -> String) -> (CoreBndr -> OccName) -> CoreBndr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreBndr -> OccName
forall name. HasOccName name => name -> OccName
occName) (CoreBind -> [CoreBndr]
forall b. Bind b -> [b]
bindersOf CoreBind
r)
doAssoc :: InferM Context
doAssoc =
do Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugging (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$ String -> InferM ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("[TRACE] Begin inferring: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bindingNames)
Context
env <- (InferEnv -> Context) -> InferM Context
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> Context
varEnv
(ctx :: Context
ctx, cs :: ConstraintSetF Atomic
cs) <- InferM Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Context, ConstraintSetF Atomic)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (InferM Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Context, ConstraintSetF Atomic))
-> InferM Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Context, ConstraintSetF Atomic)
forall a b. (a -> b) -> a -> b
$ CoreBind -> InferM Context
inferRec CoreBind
r
let satAction :: SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
satAction s :: SchemeGen d
s =
do ConstraintSetF Atomic
cs' <- (SchemeGen d, ConstraintSetF Atomic) -> ConstraintSetF Atomic
forall a b. (a, b) -> b
snd ((SchemeGen d, ConstraintSetF Atomic) -> ConstraintSetF Atomic)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen d, ConstraintSetF Atomic)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(ConstraintSetF Atomic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen d, ConstraintSetF Atomic)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen d, ConstraintSetF Atomic))
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen d, ConstraintSetF Atomic)
forall a b. (a -> b) -> a -> b
$ RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
forall a. Refined a => InferM a -> InferM a
saturate (do { ConstraintSetF Atomic -> InferM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ConstraintSetF Atomic
cs; SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
forall (m :: * -> *) a. Monad m => a -> m a
return SchemeGen d
s }))
ConstraintSetF Atomic
es <- ConstraintSetF Atomic
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(ConstraintSetF Atomic)
cexs ConstraintSetF Atomic
cs'
SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
forall (m :: * -> *) a. Monad m => a -> m a
return (SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d))
-> SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
forall a b. (a -> b) -> a -> b
$ SchemeGen d
s {
boundvs :: Domain
boundvs = (ConstraintSetF Atomic -> Domain
forall t. Refined t => t -> Domain
domain ConstraintSetF Atomic
cs' Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> SchemeGen d -> Domain
forall t. Refined t => t -> Domain
domain SchemeGen d
s) Domain -> Domain -> Domain
I.\\ Context -> Domain
forall t. Refined t => t -> Domain
domain Context
env,
constraints :: ConstraintSetF Atomic
Scheme.constraints = ConstraintSetF Atomic
es ConstraintSetF Atomic
-> ConstraintSetF Atomic -> ConstraintSetF Atomic
forall a. Semigroup a => a -> a -> a
<> ConstraintSetF Atomic
cs'
}
Context
ctx' <- (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> Context -> InferM Context
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall d.
Outputable d =>
SchemeGen d
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity (SchemeGen d)
satAction Context
ctx
let es :: ConstraintSetF Atomic
es = (ConstraintSetF Atomic -> SchemeGen TyCon -> ConstraintSetF Atomic)
-> ConstraintSetF Atomic -> Context -> ConstraintSetF Atomic
forall a b k. (a -> b -> a) -> a -> Map k b -> a
M.foldl' (\ss :: ConstraintSetF Atomic
ss sch :: SchemeGen TyCon
sch -> SchemeGen TyCon -> ConstraintSetF Atomic
Scheme.unsats SchemeGen TyCon
sch ConstraintSetF Atomic
-> ConstraintSetF Atomic -> ConstraintSetF Atomic
forall a. Semigroup a => a -> a -> a
<> ConstraintSetF Atomic
ss) ConstraintSetF Atomic
forall a. Monoid a => a
mempty Context
ctx'
ConstraintSetF Atomic -> InferM ()
noteErrs ConstraintSetF Atomic
es
Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugging (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$ String -> InferM ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("[TRACE] End inferring: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bindingNames)
InferM ()
incrN
Context -> InferM Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
ctx'
inferRec :: CoreBind -> InferM Context
inferRec :: CoreBind -> InferM Context
inferRec (NonRec x :: CoreBndr
x e :: Expr CoreBndr
e) = Name -> SchemeGen TyCon -> Context
forall k a. k -> a -> Map k a
M.singleton (CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
x) (SchemeGen TyCon -> Context)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
inferRec (Rec xes :: [(CoreBndr, Expr CoreBndr)]
xes) = do
Map Name (Expr CoreBndr, SchemeGen TyCon)
binds <-
Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Map Name (Expr CoreBndr, SchemeGen TyCon))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
(Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Map Name (Expr CoreBndr, SchemeGen TyCon)))
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Map Name (Expr CoreBndr, SchemeGen TyCon))
forall a b. (a -> b) -> a -> b
$ [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
([(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon)))
-> [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
forall a b. (a -> b) -> a -> b
$ (CoreBndr -> Name)
-> (Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
-> (CoreBndr, Expr CoreBndr)
-> (Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName
( \e :: Expr CoreBndr
e -> do
SchemeGen TyCon
rec_scheme <- Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
freshCoreScheme (Expr CoreBndr -> Type
exprType Expr CoreBndr
e)
(Expr CoreBndr, SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr CoreBndr
e, SchemeGen TyCon
rec_scheme)
)
((CoreBndr, Expr CoreBndr)
-> (Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon)))
-> [(CoreBndr, Expr CoreBndr)]
-> [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Expr CoreBndr, SchemeGen TyCon))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(CoreBndr, Expr CoreBndr)]
xes
Context -> InferM Context -> InferM Context
forall a. Context -> InferM a -> InferM a
putVars (((Expr CoreBndr, SchemeGen TyCon) -> SchemeGen TyCon)
-> Map Name (Expr CoreBndr, SchemeGen TyCon) -> Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr CoreBndr, SchemeGen TyCon) -> SchemeGen TyCon
forall a b. (a, b) -> b
snd Map Name (Expr CoreBndr, SchemeGen TyCon)
binds) (InferM Context -> InferM Context)
-> InferM Context -> InferM Context
forall a b. (a -> b) -> a -> b
$
((Expr CoreBndr, SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> Map Name (Expr CoreBndr, SchemeGen TyCon) -> InferM Context
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
( \(e :: Expr CoreBndr
e, rec_scheme :: SchemeGen TyCon
rec_scheme) -> do
SchemeGen TyCon
scheme <- Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
Type -> Type -> InferM ()
inferSubType (SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
body SchemeGen TyCon
scheme) (SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
body SchemeGen TyCon
rec_scheme)
Type -> Type -> InferM ()
inferSubType (SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
body SchemeGen TyCon
rec_scheme) (SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
body SchemeGen TyCon
scheme)
SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return SchemeGen TyCon
scheme
)
Map Name (Expr CoreBndr, SchemeGen TyCon)
binds
infer :: CoreExpr -> InferM Scheme
infer :: Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer (Core.Var v :: CoreBndr
v) =
case CoreBndr -> Maybe DataCon
isDataConId_maybe CoreBndr
v of
Just k :: DataCon
k
| TyCon -> Bool
isClassTyCon (TyCon -> Bool) -> TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
dataConTyCon DataCon
k -> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] Type
forall d. TypeGen d
Ambiguous)
| Bool
otherwise -> DataCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
fromCoreCons DataCon
k
Nothing -> CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
getVar CoreBndr
v
infer l :: Expr CoreBndr
l@(Core.Lit _) = Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
freshCoreScheme (Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ Expr CoreBndr -> Type
exprType Expr CoreBndr
l
infer (Core.App e1 :: Expr CoreBndr
e1 (Core.Type e2 :: Type
e2)) = do
Type
t <- Type -> InferM Type
freshCoreType Type
e2
SchemeGen TyCon
scheme <- Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e1
case SchemeGen TyCon
scheme of
Forall (a :: Name
a : as :: [Name]
as) b :: Type
b ->
SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [Name]
as (Name -> Type -> Type -> Type
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a Type
t Type
b)
Forall [] Ambiguous -> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] Type
forall d. TypeGen d
Ambiguous)
_ -> String
-> SDoc
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "Type application to monotype!" ((SchemeGen TyCon, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SchemeGen TyCon
scheme, Type
e2))
infer (Core.App e1 :: Expr CoreBndr
e1 e2 :: Expr CoreBndr
e2) =
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Refined a => InferM a -> InferM a
saturate
( Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e1 RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Forall as :: [Name]
as Ambiguous -> [Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [Name]
as Type
forall d. TypeGen d
Ambiguous SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e2
Forall as :: [Name]
as (t3 :: Type
t3 :=> t4 :: Type
t4) -> do
Type
t2 <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e2
Type -> Type -> InferM ()
inferSubType Type
t2 Type
t3
SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [Name]
as Type
t4
_ -> String
-> SDoc
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "The expression has been given too many arguments!" (SDoc
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> SDoc
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ (Type, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Expr CoreBndr -> Type
exprType Expr CoreBndr
e1, Expr CoreBndr -> Type
exprType Expr CoreBndr
e2)
)
infer (Core.Lam x :: CoreBndr
x e :: Expr CoreBndr
e)
| CoreBndr -> Bool
isTyVar CoreBndr
x = do
Name
a <- CoreBndr -> InferM Name
forall a. NamedThing a => a -> InferM Name
getExternalName CoreBndr
x
Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Forall as :: [Name]
as t :: Type
t -> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall (Name
a Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
as) Type
t
| Bool
otherwise = do
Type
t1 <- Type -> InferM Type
freshCoreType (CoreBndr -> Type
varType CoreBndr
x)
Name
-> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Name -> SchemeGen TyCon -> InferM a -> InferM a
putVar (CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
x) ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] Type
t1) (Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e) RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Forall as :: [Name]
as t2 :: Type
t2 -> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [Name]
as (Type
t1 Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
:=> Type
t2)
infer (Core.Let b :: CoreBind
b e :: Expr CoreBndr
e) = RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Refined a => InferM a -> InferM a
saturate (RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ do
Context
ts <- CoreBind -> InferM Context
associate CoreBind
b
Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Context -> InferM a -> InferM a
putVars Context
ts (RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
infer (Core.Case e :: Expr CoreBndr
e bind_e :: CoreBndr
bind_e core_ret :: Type
core_ret alts :: [Alt CoreBndr]
alts) = RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Refined a => InferM a -> InferM a
saturate (RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ do
Type
ret <- Type -> InferM Type
freshCoreType Type
core_ret
Type
t0 <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
Name -> SchemeGen TyCon -> InferM () -> InferM ()
forall a. Name -> SchemeGen TyCon -> InferM a -> InferM a
putVar (CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
bind_e) ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] Type
t0) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
case Type
t0 of
Data dt :: DataType TyCon
dt as :: [Type]
as -> do
[DataCon]
ks <-
(Alt CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Maybe DataCon))
-> [Alt CoreBndr]
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity [DataCon]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM
( \case
(Core.DataAlt k :: DataCon
k, xs :: [CoreBndr]
xs, rhs :: Expr CoreBndr
rhs)
| Bool -> Bool
not (Expr CoreBndr -> Bool
isBottoming Expr CoreBndr
rhs) -> do
RVar
y <- InferM RVar
fresh
Context
ts <-
case DataType TyCon
dt of
Inj x :: RVar
x _ -> [(Name, SchemeGen TyCon)] -> Context
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, SchemeGen TyCon)] -> Context)
-> ([SchemeGen TyCon] -> [(Name, SchemeGen TyCon)])
-> [SchemeGen TyCon]
-> Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [SchemeGen TyCon] -> [(Name, SchemeGen TyCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CoreBndr -> Name) -> [CoreBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName [CoreBndr]
xs) ([SchemeGen TyCon] -> Context)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
[SchemeGen TyCon]
-> InferM Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> SchemeGen TyCon) -> [Type] -> [SchemeGen TyCon]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall []) ([Type] -> [SchemeGen TyCon])
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
[SchemeGen TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RVar
-> [Type]
-> DataCon
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
consInstArgs RVar
x [Type]
as DataCon
k))
Base _ -> [(Name, SchemeGen TyCon)] -> Context
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, SchemeGen TyCon)] -> Context)
-> ([SchemeGen TyCon] -> [(Name, SchemeGen TyCon)])
-> [SchemeGen TyCon]
-> Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [SchemeGen TyCon] -> [(Name, SchemeGen TyCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CoreBndr -> Name) -> [CoreBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName [CoreBndr]
xs) ([SchemeGen TyCon] -> Context)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
[SchemeGen TyCon]
-> InferM Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> SchemeGen TyCon) -> [Type] -> [SchemeGen TyCon]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall []) ([Type] -> [SchemeGen TyCon])
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
[SchemeGen TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RVar
-> [Type]
-> DataCon
-> RWST InferEnv (ConstraintSetF Atomic) InferState Identity [Type]
consInstArgs RVar
y [Type]
as DataCon
k))
[DataCon] -> DataType TyCon -> InferM () -> InferM ()
forall a. [DataCon] -> DataType TyCon -> InferM a -> InferM a
branchAny [DataCon
k] DataType TyCon
dt (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$ do
Type
ret_i <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Context -> InferM a -> InferM a
putVars Context
ts (Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
rhs)
Type -> Type -> InferM ()
inferSubType Type
ret_i Type
ret
Maybe DataCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Maybe DataCon)
forall (m :: * -> *) a. Monad m => a -> m a
return (DataCon -> Maybe DataCon
forall a. a -> Maybe a
Just DataCon
k)
(Core.LitAlt _, _, rhs :: Expr CoreBndr
rhs)
| Bool -> Bool
not (Expr CoreBndr -> Bool
isBottoming Expr CoreBndr
rhs) -> do
Type
ret_i <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
rhs
Type -> Type -> InferM ()
inferSubType Type
ret_i Type
ret
Maybe DataCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Maybe DataCon)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DataCon
forall a. Maybe a
Nothing
_ -> Maybe DataCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(Maybe DataCon)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DataCon
forall a. Maybe a
Nothing
)
[Alt CoreBndr]
alts
case [Alt CoreBndr] -> ([Alt CoreBndr], Maybe (Expr CoreBndr))
forall a b. [(AltCon, [a], b)] -> ([(AltCon, [a], b)], Maybe b)
findDefault [Alt CoreBndr]
alts of
(_, Just rhs :: Expr CoreBndr
rhs) | Bool -> Bool
not (Expr CoreBndr -> Bool
isBottoming Expr CoreBndr
rhs) ->
[DataCon] -> DataType TyCon -> InferM () -> InferM ()
forall a. [DataCon] -> DataType TyCon -> InferM a -> InferM a
branchAny (TyCon -> [DataCon]
tyConDataCons (DataType TyCon -> TyCon
forall d. DataType d -> d
tyconOf DataType TyCon
dt) [DataCon] -> [DataCon] -> [DataCon]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [DataCon]
ks) DataType TyCon
dt (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$ do
Type
ret_i <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
rhs
Type -> Type -> InferM ()
inferSubType Type
ret_i Type
ret
_ | (Inj x :: RVar
x d :: TyCon
d) <- DataType TyCon
dt -> do
SrcSpan
l <- (InferEnv -> SrcSpan)
-> RWST
InferEnv (ConstraintSetF Atomic) InferState Identity SrcSpan
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> SrcSpan
inferLoc
DataType TyCon -> [DataCon] -> SrcSpan -> InferM ()
emitDK (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d) [DataCon]
ks SrcSpan
l
_ -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ ->
(Alt CoreBndr -> InferM ()) -> [Alt CoreBndr] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
( \(_, xs :: [CoreBndr]
xs, rhs :: Expr CoreBndr
rhs) ->
do
Context
ts <- Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> InferM Context
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> InferM Context)
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> InferM Context
forall a b. (a -> b) -> a -> b
$ [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)))
-> [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))]
-> Map
Name
(RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
forall a b. (a -> b) -> a -> b
$ [Name]
-> [RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)]
-> [(Name,
RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CoreBndr -> Name) -> [CoreBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName [CoreBndr]
xs) ((CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> [CoreBndr]
-> [RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
freshCoreScheme (Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> (CoreBndr -> Type)
-> CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreBndr -> Type
varType) [CoreBndr]
xs)
Type
ret_i <- SchemeGen TyCon -> Type
forall d. SchemeGen d -> TypeGen d
mono (SchemeGen TyCon -> Type)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. Context -> InferM a -> InferM a
putVars Context
ts (Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
rhs)
Type -> Type -> InferM ()
inferSubType Type
ret_i Type
ret
)
[Alt CoreBndr]
alts
SchemeGen TyCon
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Type -> SchemeGen TyCon
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] Type
ret)
infer (Core.Cast e :: Expr CoreBndr
e g :: Coercion
g) = do
SchemeGen TyCon
_ <- Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
freshCoreScheme (Pair Type -> Type
forall a. Pair a -> a
pSnd (Pair Type -> Type) -> Pair Type -> Type
forall a b. (a -> b) -> a -> b
$ Coercion -> Pair Type
coercionKind Coercion
g)
infer (Core.Tick SourceNote {sourceSpan :: forall id. Tickish id -> RealSrcSpan
sourceSpan = RealSrcSpan
s} e :: Expr CoreBndr
e) = SrcSpan
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. SrcSpan -> InferM a -> InferM a
setLoc (RealSrcSpan -> SrcSpan
RealSrcSpan RealSrcSpan
s) (RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon))
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a b. (a -> b) -> a -> b
$ Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
infer (Core.Tick _ e :: Expr CoreBndr
e) = Expr CoreBndr
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
infer Expr CoreBndr
e
infer (Core.Coercion g :: Coercion
g) = Type
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
freshCoreScheme (Pair Type -> Type
forall a. Pair a -> a
pSnd (Pair Type -> Type) -> Pair Type -> Type
forall a b. (a -> b) -> a -> b
$ Coercion -> Pair Type
coercionKind Coercion
g)
infer (Core.Type t :: Type
t) = String
-> SDoc
-> RWST
InferEnv
(ConstraintSetF Atomic)
InferState
Identity
(SchemeGen TyCon)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "Unexpected type" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
isBottoming :: CoreExpr -> Bool
isBottoming :: Expr CoreBndr -> Bool
isBottoming e :: Expr CoreBndr
e =
case Expr CoreBndr -> Maybe (RVar, StrictSig)
exprBotStrictness_maybe Expr CoreBndr
e of
Nothing -> Expr CoreBndr -> Bool
exprIsBottom Expr CoreBndr
e
Just (_, _) -> Bool
True