{-# 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

{-|
    The type of subtype inference constraints that are accumulated
    during the subtype inference fixpoint algorithm.

    There is a 1-1 correspondence between this type and the type of
    atomic constraints, but the former contain more information
    (though this information could be determined by the context at
    great expense).
-}
type SubTyAtom = (Guard, RVar, RVar, TyCon)

{-|
    The type of elements of the frontier in the subtype inference fixpoint
    algorithm.  There is an injection from this type into the typ of atomic
    constraints, but the inhabitants of this type additionally track the
    types used to instantiate the constructors of the datatype involved in
    the constraint.  This additional information is needed to unfold the 
    frontier and look for successors.
-}
type SubTyFrontierAtom = (Guard, RVar, RVar, TyCon, [Type], [Type])

{-|
    The type of the subtype inference algorithm, i.e. a stateful fixed 
    point computation that must additionally draw upon the services of 
    the inference monad to deal with GHC types.
-}
type SubTyComputation = StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()

{-|
    Given a pair of types @t1@ and @t2@, @inferSubType t1 t2@ is the action
    that emits constraints characterising @t1 <= t2@.

    Also emits statistics on the size of the input parameters to do with slices.
-}
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  -- Entering a slice
              [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)])
              -- Note how big it was for statistics
              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)
              -- Emit a constraint for each one
              [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') =
      -- getName here is probably unnecessary, should look it up
      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 _ _ = []

-- Infer constraints for a module
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)

-- Infer a set of constraints and associate them to qualified type scheme
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 }))
                    -- Attempt to build a model and record counterexamples
                    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'
                      }
          -- add constraints to every type in the recursive group
          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
          -- note down any counterexamples
          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'

-- Infer constraints for a mutually recursive binders
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
  -- Add binds for recursive calls
  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
          -- Bound recursive calls
          -- Must be bidirectional for mututally recursive groups
          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 constraints for a program expression
infer :: CoreExpr -> InferM Scheme
infer :: Expr CoreBndr
-> RWST
     InferEnv
     (ConstraintSetF Atomic)
     InferState
     Identity
     (SchemeGen TyCon)
infer (Core.Var v :: CoreBndr
v) =
  -- Check if identifier is a constructor
  case CoreBndr -> Maybe DataCon
isDataConId_maybe CoreBndr
v of
    Just k :: DataCon
k
      -- Ignore typeclass evidence
      | 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) -- Type application
    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
        -- See FromCore 88 for the case when as /= []
        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 -- Type abstraction
  | 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
  -- Fresh return type
  Type
ret <- Type -> InferM Type
freshCoreType Type
core_ret
  -- Infer expression on which to pattern match
  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
  -- Add the variable under scrutinee to scope
  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
                    -- Add constructor arguments introduced by the pattern
                    RVar
y <- InferM RVar
fresh -- only used in Base case of ts
                    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
                      -- Ensure return type is valid
                      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
                    -- Record constructorsc
                    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
                        -- Ensure return type is valid
                        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
                      -- Record constructors
                        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 -- Skip defaults until all constructors have been seen
            )
            [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) ->
            -- Guard by unseen constructors
            [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
              -- Ensure return type is valid
              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
            -- Ensure destructor is total if not nested
            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 -- Add constructor arguments introduced by the pattern
                    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)
                    -- Ensure return type is valid
                    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 -- Track location in source text
infer (Core.Tick _ e :: Expr CoreBndr
e) = Expr CoreBndr
-> RWST
     InferEnv
     (ConstraintSetF Atomic)
     InferState
     Identity
     (SchemeGen TyCon)
infer Expr CoreBndr
e -- Ignore other ticks
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