-- | Defines type-inference algorithm.
--
-- For type inference we have to define instance of the Lang class:
--
-- > data NoPrim
-- >   deriving (Show)
-- >
-- > data TestLang
-- >
-- > instance Lang TestLang where
-- >   type Src  TestLang = ()              -- ^ define type for source code locations
-- >   type Var  TestLang = Text            -- ^ define type for variables
-- >   type Prim TestLang = NoPrim          -- ^ define type for primitive operators
-- >   getPrimType _ _ = error "No primops"   -- ^ reports types for primitives
--
-- Also we define context for type inference that holds types for all known variables
-- Often it defines types for all global variables or functions that are external.
--
-- > context = Context $ Map.fromList [...]
--
-- Then we can use inference to derive type for given term with @inferType@ or
-- we can derive types for all sub-expressions of given term with @inferTerm@.
-- See module in the test "TM.Infer" for examples of the usage.
--
-- > termI,termK :: Term NoPrim () Text
-- >
-- > -- I combinator
-- > termI = lamE () "x" $ varE () "x"
-- > -- K combinator
-- > termK = lamE () "x" $ lamE () "y" $ varE () "x"
-- >
-- > -- Let's infer types
-- > typeI = inferType mempty termI
-- > typeK = inferType mempty termK
--
-- There are functions to check that two types unify (@unifyTypes@) or that one type
-- is subtype of another one (@subtypeOf@).
module Type.Check.HM.Infer(
  -- * Context
    Context(..)
  , insertCtx
  , lookupCtx
  , insertConstructorCtx
  , lookupConstructorCtx
  , ContextOf
  -- * Inference
  , inferType
  , inferTerm
  , inferTypeList
  , inferTermList
  , subtypeOf
  , unifyTypes
  -- * Utils
  , closeSignature
  , printInfer
) where

import Control.Monad.Identity
import Control.Monad.Writer.Strict

import Control.Applicative
import Control.Arrow (second)
import Control.Monad.Except
import Control.Monad.State.Strict

import Data.Bifunctor (bimap)
import Data.Fix
import Data.Function (on)
import Data.Map.Strict (Map)
import Data.Maybe

import Type.Check.HM.Lang
import Type.Check.HM.Term
import Type.Check.HM.Subst
import Type.Check.HM.Type
import Type.Check.HM.TypeError
import Type.Check.HM.TyTerm
import Type.Check.HM.Pretty

import qualified Data.Map.Strict as M
import qualified Data.Set as S
import qualified Data.List as L

-- | Context holds map of proven signatures for free variables in the expression.
data Context loc v = Context
  { Context loc v -> Map v (Signature loc v)
context'binds         :: Map v (Signature loc v)   -- ^ known binds
  , Context loc v -> Map v (Signature loc v)
context'constructors  :: Map v (Signature loc v)   -- ^ known constructors for user-defined types
  }
  deriving (Int -> Context loc v -> ShowS
[Context loc v] -> ShowS
Context loc v -> String
(Int -> Context loc v -> ShowS)
-> (Context loc v -> String)
-> ([Context loc v] -> ShowS)
-> Show (Context loc v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall loc v. (Show v, Show loc) => Int -> Context loc v -> ShowS
forall loc v. (Show v, Show loc) => [Context loc v] -> ShowS
forall loc v. (Show v, Show loc) => Context loc v -> String
showList :: [Context loc v] -> ShowS
$cshowList :: forall loc v. (Show v, Show loc) => [Context loc v] -> ShowS
show :: Context loc v -> String
$cshow :: forall loc v. (Show v, Show loc) => Context loc v -> String
showsPrec :: Int -> Context loc v -> ShowS
$cshowsPrec :: forall loc v. (Show v, Show loc) => Int -> Context loc v -> ShowS
Show, Context loc v -> Context loc v -> Bool
(Context loc v -> Context loc v -> Bool)
-> (Context loc v -> Context loc v -> Bool) -> Eq (Context loc v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall loc v.
(Eq v, Eq loc) =>
Context loc v -> Context loc v -> Bool
/= :: Context loc v -> Context loc v -> Bool
$c/= :: forall loc v.
(Eq v, Eq loc) =>
Context loc v -> Context loc v -> Bool
== :: Context loc v -> Context loc v -> Bool
$c== :: forall loc v.
(Eq v, Eq loc) =>
Context loc v -> Context loc v -> Bool
Eq)

instance Ord v => Semigroup (Context loc v) where
  <> :: Context loc v -> Context loc v -> Context loc v
(<>) (Context Map v (Signature loc v)
bs1 Map v (Signature loc v)
cs1) (Context Map v (Signature loc v)
bs2 Map v (Signature loc v)
cs2) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v)
bs1 Map v (Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a. Semigroup a => a -> a -> a
<> Map v (Signature loc v)
bs2) (Map v (Signature loc v)
cs1 Map v (Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a. Semigroup a => a -> a -> a
<> Map v (Signature loc v)
cs2)

instance Ord v => Monoid (Context loc v) where
  mempty :: Context loc v
mempty = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context Map v (Signature loc v)
forall a. Monoid a => a
mempty Map v (Signature loc v)
forall a. Monoid a => a
mempty

-- | Type synonym for context.
type ContextOf q = Context (Src q) (Var q)

instance CanApply Context where
  apply :: Subst loc v -> Context loc v -> Context loc v
apply Subst loc v
subst Context loc v
ctx = Context loc v
ctx
      { context'binds :: Map v (Signature loc v)
context'binds = (Signature loc v -> Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst loc v -> Signature loc v -> Signature loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
subst) (Map v (Signature loc v) -> Map v (Signature loc v))
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a b. (a -> b) -> a -> b
$ Context loc v -> Map v (Signature loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds Context loc v
ctx
      }

-- | Insert signature into context
insertCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v
insertCtx :: v -> Signature loc v -> Context loc v -> Context loc v
insertCtx v
v Signature loc v
sign (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (v
-> Signature loc v
-> Map v (Signature loc v)
-> Map v (Signature loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Signature loc v
sign Map v (Signature loc v)
binds) Map v (Signature loc v)
cons

-- | Lookup signature by name in the context of inferred terms.
lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
lookupCtx :: v -> Context loc v -> Maybe (Signature loc v)
lookupCtx v
v (Context Map v (Signature loc v)
binds Map v (Signature loc v)
_cons) = v -> Map v (Signature loc v) -> Maybe (Signature loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Signature loc v)
binds

-- | Insert signature into context
insertConstructorCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v
insertConstructorCtx :: v -> Signature loc v -> Context loc v -> Context loc v
insertConstructorCtx v
v Signature loc v
sign (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context Map v (Signature loc v)
binds (v
-> Signature loc v
-> Map v (Signature loc v)
-> Map v (Signature loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Signature loc v
sign Map v (Signature loc v)
cons)

-- | Lookup signature by name in the context of inferred terms.
lookupConstructorCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx :: v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx v
v (Context Map v (Signature loc v)
_binds Map v (Signature loc v)
cons) = v -> Map v (Signature loc v) -> Maybe (Signature loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Signature loc v)
cons

-- | Wrapper with ability to generate fresh names
data Name v
  = Name v
  | FreshName !Int
  deriving (Int -> Name v -> ShowS
[Name v] -> ShowS
Name v -> String
(Int -> Name v -> ShowS)
-> (Name v -> String) -> ([Name v] -> ShowS) -> Show (Name v)
forall v. Show v => Int -> Name v -> ShowS
forall v. Show v => [Name v] -> ShowS
forall v. Show v => Name v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name v] -> ShowS
$cshowList :: forall v. Show v => [Name v] -> ShowS
show :: Name v -> String
$cshow :: forall v. Show v => Name v -> String
showsPrec :: Int -> Name v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> Name v -> ShowS
Show, Name v -> Name v -> Bool
(Name v -> Name v -> Bool)
-> (Name v -> Name v -> Bool) -> Eq (Name v)
forall v. Eq v => Name v -> Name v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name v -> Name v -> Bool
$c/= :: forall v. Eq v => Name v -> Name v -> Bool
== :: Name v -> Name v -> Bool
$c== :: forall v. Eq v => Name v -> Name v -> Bool
Eq, Eq (Name v)
Eq (Name v)
-> (Name v -> Name v -> Ordering)
-> (Name v -> Name v -> Bool)
-> (Name v -> Name v -> Bool)
-> (Name v -> Name v -> Bool)
-> (Name v -> Name v -> Bool)
-> (Name v -> Name v -> Name v)
-> (Name v -> Name v -> Name v)
-> Ord (Name v)
Name v -> Name v -> Bool
Name v -> Name v -> Ordering
Name v -> Name v -> Name v
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (Name v)
forall v. Ord v => Name v -> Name v -> Bool
forall v. Ord v => Name v -> Name v -> Ordering
forall v. Ord v => Name v -> Name v -> Name v
min :: Name v -> Name v -> Name v
$cmin :: forall v. Ord v => Name v -> Name v -> Name v
max :: Name v -> Name v -> Name v
$cmax :: forall v. Ord v => Name v -> Name v -> Name v
>= :: Name v -> Name v -> Bool
$c>= :: forall v. Ord v => Name v -> Name v -> Bool
> :: Name v -> Name v -> Bool
$c> :: forall v. Ord v => Name v -> Name v -> Bool
<= :: Name v -> Name v -> Bool
$c<= :: forall v. Ord v => Name v -> Name v -> Bool
< :: Name v -> Name v -> Bool
$c< :: forall v. Ord v => Name v -> Name v -> Bool
compare :: Name v -> Name v -> Ordering
$ccompare :: forall v. Ord v => Name v -> Name v -> Ordering
$cp1Ord :: forall v. Ord v => Eq (Name v)
Ord)

fromNameVar :: Name v -> Either (TypeError loc v) v
fromNameVar :: Name v -> Either (TypeError loc v) v
fromNameVar = \case
  Name v
v      -> v -> Either (TypeError loc v) v
forall a b. b -> Either a b
Right v
v
  FreshName Int
_ -> TypeError loc v -> Either (TypeError loc v) v
forall a b. a -> Either a b
Left TypeError loc v
forall loc var. TypeError loc var
FreshNameFound

instance IsVar a => IsVar (Name a) where
  prettyLetters :: [Name a]
prettyLetters = (a -> Name a) -> [a] -> [Name a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Name a
forall v. v -> Name v
Name ([a]
forall v. IsVar v => [v]
prettyLetters :: [a])

-- Synonyms to simplify typing
type Context' loc v = Context (Origin loc) (Name v)
type Type' loc v = Type (Origin loc) (Name v)
type Signature' loc v = Signature (Origin loc) (Name v)
type Subst' loc v = Subst (Origin loc) (Name v)
type Bind' loc v a = Bind (Origin loc) (Name v) a
type VarSet' loc v = VarSet (Origin loc) (Name v)

type ContextOf' q = Context (Origin (Src q)) (Name (Var q))
type TypeOf' q = Type (Origin (Src q)) (Name (Var q))
type TermOf' q = Term (Prim q) (Origin (Src q)) (Name (Var q))
type TyTermOf' q = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
type SignatureOf' q = Signature (Origin (Src q)) (Name (Var q))
type SubstOf' q = Subst (Origin (Src q)) (Name (Var q))
type BindOf' q a = Bind (Origin (Src q)) (Name (Var q)) a
type CaseAltOf' q = CaseAlt (Origin (Src q)) (Name (Var q))

-- | We leave in the context only terms that are truly needed.
-- To check the term we need only variables that are free in the term.
-- So we can safely remove everything else and speed up lookup times.
restrictContext :: Ord v => Term prim loc v -> Context loc v -> Context loc v
restrictContext :: Term prim loc v -> Context loc v -> Context loc v
restrictContext Term prim loc v
t (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Map v () -> Map v (Signature loc v)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.intersection Map v (Signature loc v)
binds Map v ()
fv) Map v (Signature loc v)
cons
  where
    fv :: Map v ()
fv = [(v, ())] -> Map v ()
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(v, ())] -> Map v ()) -> [(v, ())] -> Map v ()
forall a b. (a -> b) -> a -> b
$ (v -> (v, ())) -> [v] -> [(v, ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, ()) ([v] -> [(v, ())]) -> [v] -> [(v, ())]
forall a b. (a -> b) -> a -> b
$ Set v -> [v]
forall a. Set a -> [a]
S.toList (Set v -> [v]) -> Set v -> [v]
forall a b. (a -> b) -> a -> b
$ Term prim loc v -> Set v
forall v prim loc. Ord v => Term prim loc v -> Set v
freeVars Term prim loc v
t

wrapContextNames :: Ord v => Context loc v -> Context loc (Name v)
wrapContextNames :: Context loc v -> Context loc (Name v)
wrapContextNames = (v -> Name v) -> Context loc v -> Context loc (Name v)
forall v k1 loc.
Ord v =>
(k1 -> v) -> Context loc k1 -> Context loc v
fmapCtx v -> Name v
forall v. v -> Name v
Name
  where
    fmapCtx :: (k1 -> v) -> Context loc k1 -> Context loc v
fmapCtx k1 -> v
f (Context Map k1 (Signature loc k1)
bs Map k1 (Signature loc k1)
cs) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap Map k1 (Signature loc k1)
bs)  (Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap Map k1 (Signature loc k1)
cs)
      where
        wrap :: Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap = (k1 -> v) -> Map k1 (Signature loc v) -> Map v (Signature loc v)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys k1 -> v
f (Map k1 (Signature loc v) -> Map v (Signature loc v))
-> (Map k1 (Signature loc k1) -> Map k1 (Signature loc v))
-> Map k1 (Signature loc k1)
-> Map v (Signature loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signature loc k1 -> Signature loc v)
-> Map k1 (Signature loc k1) -> Map k1 (Signature loc v)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((k1 -> v) -> Signature loc k1 -> Signature loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap k1 -> v
f)

wrapTermNames :: Term prim loc v -> Term prim loc (Name v)
wrapTermNames :: Term prim loc v -> Term prim loc (Name v)
wrapTermNames = (v -> Name v) -> Term prim loc v -> Term prim loc (Name v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name

markProven :: Context loc v -> Context (Origin loc) v
markProven :: Context loc v -> Context (Origin loc) v
markProven (Context Map v (Signature loc v)
bs Map v (Signature loc v)
cs) = Map v (Signature (Origin loc) v)
-> Map v (Signature (Origin loc) v) -> Context (Origin loc) v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Map v (Signature (Origin loc) v)
forall k a var.
Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark Map v (Signature loc v)
bs) (Map v (Signature loc v) -> Map v (Signature (Origin loc) v)
forall k a var.
Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark Map v (Signature loc v)
cs)
  where
    mark :: Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark = (Signature a var -> Signature (Origin a) var)
-> Map k (Signature a var) -> Map k (Signature (Origin a) var)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((a -> Origin a) -> Signature a var -> Signature (Origin a) var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc a -> Origin a
forall a. a -> Origin a
Proven)

markUserCode :: Term prim loc v -> Term prim (Origin loc) v
markUserCode :: Term prim loc v -> Term prim (Origin loc) v
markUserCode = (loc -> Origin loc) -> Term prim loc v -> Term prim (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode

chooseUserOrigin :: Show a => Origin a -> Origin a -> a
chooseUserOrigin :: Origin a -> Origin a -> a
chooseUserOrigin Origin a
x Origin a
y = case (Origin a
x, Origin a
y) of
  (UserCode a
a, Origin a
_) -> a
a
  (Origin a
_, UserCode a
a) -> a
a
  (Origin a, Origin a)
_               -> Origin a -> a
forall a. Origin a -> a
fromOrigin Origin a
x

-- | Type-tag for source locations to distinguish proven types from those
-- that have to be checked.
--
-- We use it on unification failure to show source locations in the user code and not in the
-- expression that is already was proven.
data Origin a
  = Proven a
  -- ^ Proven source code location
  | UserCode a
  -- ^ User source code (we type-check it)
  deriving (Int -> Origin a -> ShowS
[Origin a] -> ShowS
Origin a -> String
(Int -> Origin a -> ShowS)
-> (Origin a -> String) -> ([Origin a] -> ShowS) -> Show (Origin a)
forall a. Show a => Int -> Origin a -> ShowS
forall a. Show a => [Origin a] -> ShowS
forall a. Show a => Origin a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Origin a] -> ShowS
$cshowList :: forall a. Show a => [Origin a] -> ShowS
show :: Origin a -> String
$cshow :: forall a. Show a => Origin a -> String
showsPrec :: Int -> Origin a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Origin a -> ShowS
Show, a -> Origin b -> Origin a
(a -> b) -> Origin a -> Origin b
(forall a b. (a -> b) -> Origin a -> Origin b)
-> (forall a b. a -> Origin b -> Origin a) -> Functor Origin
forall a b. a -> Origin b -> Origin a
forall a b. (a -> b) -> Origin a -> Origin b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Origin b -> Origin a
$c<$ :: forall a b. a -> Origin b -> Origin a
fmap :: (a -> b) -> Origin a -> Origin b
$cfmap :: forall a b. (a -> b) -> Origin a -> Origin b
Functor)

fromOrigin :: Origin a -> a
fromOrigin :: Origin a -> a
fromOrigin = \case
  Proven   a
a -> a
a
  UserCode a
a -> a
a

instance Eq a => Eq (Origin a) where
  == :: Origin a -> Origin a -> Bool
(==) = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool) -> (Origin a -> a) -> Origin a -> Origin a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Origin a -> a
forall a. Origin a -> a
fromOrigin

instance Ord a => Ord (Origin a) where
  compare :: Origin a -> Origin a -> Ordering
compare = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering)
-> (Origin a -> a) -> Origin a -> Origin a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Origin a -> a
forall a. Origin a -> a
fromOrigin

instance HasLoc a => HasLoc (Origin a) where
  type Loc (Origin a) = Loc a
  getLoc :: Origin a -> Loc (Origin a)
getLoc = a -> Loc a
forall f. HasLoc f => f -> Loc f
getLoc (a -> Loc a) -> (Origin a -> a) -> Origin a -> Loc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Origin a -> a
forall a. Origin a -> a
fromOrigin

-- | Type-inference monad.
-- Contains integer counter for fresh variables and possibility to report type-errors.
newtype InferM loc var a = InferM (StateT Int (Writer [TypeError loc (Name var)]) a)
  deriving (a -> InferM loc var b -> InferM loc var a
(a -> b) -> InferM loc var a -> InferM loc var b
(forall a b. (a -> b) -> InferM loc var a -> InferM loc var b)
-> (forall a b. a -> InferM loc var b -> InferM loc var a)
-> Functor (InferM loc var)
forall a b. a -> InferM loc var b -> InferM loc var a
forall a b. (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a b. a -> InferM loc var b -> InferM loc var a
forall loc var a b.
(a -> b) -> InferM loc var a -> InferM loc var b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> InferM loc var b -> InferM loc var a
$c<$ :: forall loc var a b. a -> InferM loc var b -> InferM loc var a
fmap :: (a -> b) -> InferM loc var a -> InferM loc var b
$cfmap :: forall loc var a b.
(a -> b) -> InferM loc var a -> InferM loc var b
Functor, Functor (InferM loc var)
a -> InferM loc var a
Functor (InferM loc var)
-> (forall a. a -> InferM loc var a)
-> (forall a b.
    InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b)
-> (forall a b c.
    (a -> b -> c)
    -> InferM loc var a -> InferM loc var b -> InferM loc var c)
-> (forall a b.
    InferM loc var a -> InferM loc var b -> InferM loc var b)
-> (forall a b.
    InferM loc var a -> InferM loc var b -> InferM loc var a)
-> Applicative (InferM loc var)
InferM loc var a -> InferM loc var b -> InferM loc var b
InferM loc var a -> InferM loc var b -> InferM loc var a
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall a. a -> InferM loc var a
forall loc var. Functor (InferM loc var)
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a. a -> InferM loc var a
forall a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall loc var a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: InferM loc var a -> InferM loc var b -> InferM loc var a
$c<* :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
*> :: InferM loc var a -> InferM loc var b -> InferM loc var b
$c*> :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
liftA2 :: (a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
$cliftA2 :: forall loc var a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
<*> :: InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
$c<*> :: forall loc var a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
pure :: a -> InferM loc var a
$cpure :: forall loc var a. a -> InferM loc var a
$cp1Applicative :: forall loc var. Functor (InferM loc var)
Applicative, Applicative (InferM loc var)
a -> InferM loc var a
Applicative (InferM loc var)
-> (forall a b.
    InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b)
-> (forall a b.
    InferM loc var a -> InferM loc var b -> InferM loc var b)
-> (forall a. a -> InferM loc var a)
-> Monad (InferM loc var)
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a. a -> InferM loc var a
forall loc var. Applicative (InferM loc var)
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
forall loc var a. a -> InferM loc var a
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall loc var a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> InferM loc var a
$creturn :: forall loc var a. a -> InferM loc var a
>> :: InferM loc var a -> InferM loc var b -> InferM loc var b
$c>> :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
>>= :: InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
$c>>= :: forall loc var a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
$cp1Monad :: forall loc var. Applicative (InferM loc var)
Monad, MonadState Int, MonadWriter [TypeError loc (Name var)])

-- | Runs inference monad.
runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM (InferM StateT Int (Writer [TypeError loc (Name var)]) a
m) = case Writer [TypeError loc (Name var)] a
-> (a, [TypeError loc (Name var)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [TypeError loc (Name var)] a
 -> (a, [TypeError loc (Name var)]))
-> Writer [TypeError loc (Name var)] a
-> (a, [TypeError loc (Name var)])
forall a b. (a -> b) -> a -> b
$ StateT Int (Writer [TypeError loc (Name var)]) a
-> Int -> Writer [TypeError loc (Name var)] a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT Int (Writer [TypeError loc (Name var)]) a
m Int
0 of
  (a
res, []) -> a -> Either [TypeError loc (Name var)] a
forall a b. b -> Either a b
Right a
res
  (a
_, [TypeError loc (Name var)]
errs) -> [TypeError loc (Name var)] -> Either [TypeError loc (Name var)] a
forall a b. a -> Either a b
Left [TypeError loc (Name var)]
errs

type InferOf q = InferM (Src q) (Var q) (Out (Prim q) (Src q) (Var q))

-- | Type-inference function.
-- We provide a context of already proven type-signatures and term to infer the type.
inferType :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TypeOf q)
inferType :: ContextOf q -> TermOf q -> Either [ErrorOf q] (TypeOf q)
inferType ContextOf q
ctx TermOf q
term = (TyTerm (Prim q) (Src q) (Var q) -> TypeOf q)
-> Either [ErrorOf q] (TyTerm (Prim q) (Src q) (Var q))
-> Either [ErrorOf q] (TypeOf q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm (Prim q) (Src q) (Var q) -> TypeOf q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType (Either [ErrorOf q] (TyTerm (Prim q) (Src q) (Var q))
 -> Either [ErrorOf q] (TypeOf q))
-> Either [ErrorOf q] (TyTerm (Prim q) (Src q) (Var q))
-> Either [ErrorOf q] (TypeOf q)
forall a b. (a -> b) -> a -> b
$ ContextOf q
-> TermOf q -> Either [ErrorOf q] (TyTerm (Prim q) (Src q) (Var q))
forall q.
Lang q =>
ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm ContextOf q
ctx TermOf q
term

-- | Infers types for all subexpressions of the given term.
-- We provide a context of already proven type-signatures and term to infer the type.
inferTerm :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm :: ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm ContextOf q
ctx TermOf q
term =
  case InferM
  (Src q)
  (Var q)
  (Subst (Origin (Src q)) (Name (Var q)),
   TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either
     [TypeError (Src q) (Name (Var q))]
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall loc var a.
InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM (InferM
   (Src q)
   (Var q)
   (Subst (Origin (Src q)) (Name (Var q)),
    TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
 -> Either
      [TypeError (Src q) (Name (Var q))]
      (Subst (Origin (Src q)) (Name (Var q)),
       TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either
     [TypeError (Src q) (Name (Var q))]
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ ContextOf' q
-> TermOf' q
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer (Context (Origin (Src q)) (Var q) -> ContextOf' q
forall v loc. Ord v => Context loc v -> Context loc (Name v)
wrapContextNames (Context (Origin (Src q)) (Var q) -> ContextOf' q)
-> Context (Origin (Src q)) (Var q) -> ContextOf' q
forall a b. (a -> b) -> a -> b
$ ContextOf q -> Context (Origin (Src q)) (Var q)
forall loc v. Context loc v -> Context (Origin loc) v
markProven (ContextOf q -> Context (Origin (Src q)) (Var q))
-> ContextOf q -> Context (Origin (Src q)) (Var q)
forall a b. (a -> b) -> a -> b
$ TermOf q -> ContextOf q -> ContextOf q
forall v prim loc.
Ord v =>
Term prim loc v -> Context loc v -> Context loc v
restrictContext TermOf q
term ContextOf q
ctx) (Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q
forall prim loc v. Term prim loc v -> Term prim loc (Name v)
wrapTermNames (Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q)
-> Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q
forall a b. (a -> b) -> a -> b
$ TermOf q -> Term (Prim q) (Origin (Src q)) (Var q)
forall prim loc v. Term prim loc v -> Term prim (Origin loc) v
markUserCode TermOf q
term) of
    Right (Subst (Origin (Src q)) (Name (Var q))
_, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTerm) -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTermOf q)
forall prim.
TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
toTyTerm TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTerm
    Left [TypeError (Src q) (Name (Var q))]
errs -> [ErrorOf q] -> Either [ErrorOf q] (TyTermOf q)
forall a b. a -> Either a b
Left ([ErrorOf q] -> Either [ErrorOf q] (TyTermOf q))
-> [ErrorOf q] -> Either [ErrorOf q] (TyTermOf q)
forall a b. (a -> b) -> a -> b
$ (TypeError (Src q) (Name (Var q)) -> ErrorOf q)
-> [TypeError (Src q) (Name (Var q))] -> [ErrorOf q]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeError (Src q) (Name (Var q)) -> ErrorOf q
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError (Src q) (Name (Var q)) -> ErrorOf q)
-> (TypeError (Src q) (Name (Var q))
    -> TypeError (Src q) (Name (Var q)))
-> TypeError (Src q) (Name (Var q))
-> ErrorOf q
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError (Src q) (Name (Var q))
-> TypeError (Src q) (Name (Var q))
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) [TypeError (Src q) (Name (Var q))]
errs
  where
    toTyTerm :: TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
toTyTerm = (ErrorOf q -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Src q) (Var q)
    -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([ErrorOf q] -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a b. a -> Either a b
Left ([ErrorOf q] -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (ErrorOf q -> [ErrorOf q])
-> ErrorOf q
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorOf q -> [ErrorOf q]
forall (f :: * -> *) a. Applicative f => a -> f a
pure) TyTerm prim (Src q) (Var q)
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a b. b -> Either a b
Right (Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
 -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
    -> Either (ErrorOf q) (TyTerm prim (Src q) (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyTerm prim (Src q) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
forall prim loc var.
TyTerm prim loc (Name var)
-> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar (TyTerm prim (Src q) (Name (Var q))
 -> Either (ErrorOf q) (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
    -> TyTerm prim (Src q) (Name (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyTerm prim (Src q) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType (TyTerm prim (Src q) (Name (Var q))
 -> TyTerm prim (Src q) (Name (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
    -> TyTerm prim (Src q) (Name (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Origin (Src q) -> Src q)
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin

type Out prim loc var = ( Subst (Origin loc) (Name var)
                        , TyTerm prim (Origin loc) (Name var)
                        )

-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.
inferTermList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList :: ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs = case [Bind (Src q) (Var q) (TermOf q)]
defs of
  []  -> [Bind (Src q) (Var q) (TyTermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  Bind (Src q) (Var q) (TermOf q)
d:[Bind (Src q) (Var q) (TermOf q)]
_ ->
    let topLoc :: Src q
topLoc = Bind (Src q) (Var q) (TermOf q) -> Src q
forall loc var a. Bind loc var a -> loc
bind'loc Bind (Src q) (Var q) (TermOf q)
d
    in  (TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)])
-> Either [ErrorOf q] (TyTermOf q)
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)]
fromLetExpr (Either [ErrorOf q] (TyTermOf q)
 -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)])
-> Either [ErrorOf q] (TyTermOf q)
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall a b. (a -> b) -> a -> b
$ ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
forall q.
Lang q =>
ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm ContextOf q
ctx (Src q -> [Bind (Src q) (Var q) (TermOf q)] -> TermOf q
forall loc v prim.
loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v
toLetExpr Src q
topLoc [Bind (Src q) (Var q) (TermOf q)]
defs)
  where
    toLetExpr :: loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v
toLetExpr loc
loc [Bind loc v (Term prim loc v)]
ds = loc
-> [Bind loc v (Term prim loc v)]
-> Term prim loc v
-> Term prim loc v
forall loc v prim.
loc
-> [Bind loc v (Term prim loc v)]
-> Term prim loc v
-> Term prim loc v
letRecE loc
loc ((Bind loc v (Term prim loc v) -> Bind loc v (Term prim loc v))
-> [Bind loc v (Term prim loc v)] -> [Bind loc v (Term prim loc v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bind loc v (Term prim loc v) -> Bind loc v (Term prim loc v)
forall a. a -> a
toBind [Bind loc v (Term prim loc v)]
ds) (loc -> Term prim loc v
forall loc prim v. loc -> Term prim loc v
bottomE loc
loc)

    fromLetExpr :: TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)]
fromLetExpr = \case
      (TyTerm (Fix (Ann Type (Src q) (Var q)
_ (LetRec Src q
_ [Bind
   (Src q)
   (Var q)
   (Fix
      (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
bs Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q)))
_)))) -> (Bind
   (Src q)
   (Var q)
   (Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))
 -> Bind (Src q) (Var q) (TyTermOf q))
-> [Bind
      (Src q)
      (Var q)
      (Fix
         (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
-> [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bind
  (Src q)
  (Var q)
  (Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))
-> Bind (Src q) (Var q) (TyTermOf q)
forall loc v prim.
Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
fromBind [Bind
   (Src q)
   (Var q)
   (Fix
      (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
bs
      TyTermOf q
_                                      -> String -> [Bind (Src q) (Var q) (TyTermOf q)]
forall a. HasCallStack => String -> a
error String
"Imposible happened. Found non let-rec expression"

    toBind :: a -> a
toBind = a -> a
forall a. a -> a
id
    fromBind :: Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
fromBind = (Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v)
-> Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm

-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.
-- It returns only top-level types for all terms.
inferTypeList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
inferTypeList :: ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
inferTypeList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs = ([Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
 -> [Bind (Src q) (Var q) (TypeOf q)])
-> Either
     [ErrorOf q]
     [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))
 -> Bind (Src q) (Var q) (TypeOf q))
-> [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> [Bind (Src q) (Var q) (TypeOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyTerm (Prim q) (Src q) (Var q) -> TypeOf q)
-> Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))
-> Bind (Src q) (Var q) (TypeOf q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm (Prim q) (Src q) (Var q) -> TypeOf q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType)) (Either
   [ErrorOf q]
   [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
 -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)])
-> Either
     [ErrorOf q]
     [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
forall a b. (a -> b) -> a -> b
$ ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either
     [ErrorOf q]
     [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
forall q.
Lang q =>
ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs

infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer :: ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx (Term (Fix TermF
  (Prim q)
  (Origin (Src q))
  (Name (Var q))
  (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
x)) = case TermF
  (Prim q)
  (Origin (Src q))
  (Name (Var q))
  (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
x of
  Var Origin (Src q)
loc Name (Var q)
v           -> ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
forall q.
Lang q =>
ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v
  Prim Origin (Src q)
loc Prim q
p          -> Origin (Src q) -> Prim q -> InferOf q
forall q. Lang q => Origin (Src q) -> Prim q -> InferOf q
inferPrim Origin (Src q)
loc Prim q
p
  App Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
b         -> ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
b)
  Lam Origin (Src q)
loc Name (Var q)
v Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
r         -> ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
r)
  Let Origin (Src q)
loc Bind
  (Origin (Src q))
  (Name (Var q))
  (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
v Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a         -> ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
inferLet ContextOf' q
ctx Origin (Src q)
loc ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> Bind
     (Origin (Src q))
     (Name (Var q))
     (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> BindOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Bind
  (Origin (Src q))
  (Name (Var q))
  (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
v) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a)
  LetRec Origin (Src q)
loc [Bind
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
vs Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a     -> ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
inferLetRec ContextOf' q
ctx Origin (Src q)
loc ((Bind
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
 -> BindOf' q (TermOf' q))
-> [Bind
      (Origin (Src q))
      (Name (Var q))
      (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
-> [BindOf' q (TermOf' q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> Bind
     (Origin (Src q))
     (Name (Var q))
     (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> BindOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term) [Bind
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
vs) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a)
  AssertType Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a Type (Origin (Src q)) (Name (Var q))
ty -> ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> Type (Origin (Src q)) (Name (Var q))
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a) Type (Origin (Src q)) (Name (Var q))
ty
  Constr Origin (Src q)
loc Name (Var q)
tag      -> ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
forall q.
Lang q =>
ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
tag
  Case Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
e [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
alts     -> ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
inferCase ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
e) ((CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
 -> CaseAltOf' q (TermOf' q))
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
-> [CaseAltOf' q (TermOf' q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> CaseAltOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term) [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
alts)
  Bottom Origin (Src q)
loc          -> Origin (Src q) -> InferOf q
forall q. Lang q => Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc

retryWithBottom :: Lang q => TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom :: TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc = do
  [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
  Origin (Src q) -> InferOf q
forall q. Lang q => Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc

inferVar :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar :: ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v = {- trace (unlines ["VAR", ppShow ctx, ppShow v]) $ -}
  case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupCtx Name (Var q)
v ContextOf' q
ctx of
    Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing  -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Name (Var q)
v) Origin (Src q)
loc
    Just Signature (Origin (Src q)) (Name (Var q))
sig -> do Type (Origin (Src q)) (Name (Var q))
ty <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance (Signature (Origin (Src q)) (Name (Var q))
 -> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q))))
-> Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Origin (Src q)
-> Signature (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) loc locA v.
LocFunctor f =>
loc -> f locA v -> f loc v
setLoc Origin (Src q)
loc Signature (Origin (Src q)) (Name (Var q))
sig
                   (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc var prim.
Type loc var -> loc -> var -> TyTerm prim loc var
tyVarE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Name (Var q)
v)

inferPrim :: Lang q => Origin (Src q) -> Prim q -> InferOf q
inferPrim :: Origin (Src q) -> Prim q -> InferOf q
inferPrim Origin (Src q)
loc Prim q
prim =
  (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Prim q
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc var prim.
Type loc var -> loc -> prim -> TyTerm prim loc var
tyPrimE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Prim q
prim)
  where
    ty :: Type (Origin (Src q)) (Name (Var q))
ty = (Var q -> Name (Var q))
-> Type (Origin (Src q)) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var q -> Name (Var q)
forall v. v -> Name v
Name (Type (Origin (Src q)) (Var q)
 -> Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ (Src q -> Origin (Src q))
-> Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Src q -> Origin (Src q)
forall a. a -> Origin a
UserCode (Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q))
-> Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q)
forall a b. (a -> b) -> a -> b
$ Src q -> Prim q -> Type (Src q) (Var q)
forall q. Lang q => Src q -> Prim q -> TypeOf q
getPrimType (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Prim q
prim

inferApp :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp :: ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp ContextOf' q
ctx Origin (Src q)
loc TermOf' q
f TermOf' q
a = {- fmap (\res -> trace (unlines ["APP", ppCtx ctx, ppShow' f, ppShow' a, ppShow' $ snd res]) res) $-} do
  Type (Origin (Src q)) (Name (Var q))
tvn <- (Name (Var q) -> Type (Origin (Src q)) (Name (Var q)))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc) (InferM (Src q) (Var q) (Name (Var q))
 -> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q))))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
  (Subst' (Src q) (Var q),
 [(Type (Origin (Src q)) (Name (Var q)),
   TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
res <- ContextOf' q
-> [TermOf' q]
-> InferM
     (Src q)
     (Var q)
     (Subst' (Src q) (Var q),
      [(Type (Origin (Src q)) (Name (Var q)),
        TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms ContextOf' q
ctx [TermOf' q
f, TermOf' q
a]
  case (Subst' (Src q) (Var q),
 [(Type (Origin (Src q)) (Name (Var q)),
   TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
res of
    (Subst' (Src q) (Var q)
phi, [(Type (Origin (Src q)) (Name (Var q))
tf, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
f'), (Type (Origin (Src q)) (Name (Var q))
ta, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
a')]) -> case Subst' (Src q) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
     (TypeError (Src q) (Name (Var q))) (Subst' (Src q) (Var q))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' (Src q) (Var q)
phi Type (Origin (Src q)) (Name (Var q))
tf (Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v. loc -> Type loc v -> Type loc v -> Type loc v
arrowT Origin (Src q)
loc Type (Origin (Src q)) (Name (Var q))
ta Type (Origin (Src q)) (Name (Var q))
tvn) of
      Left TypeError (Src q) (Name (Var q))
err    -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc
      Right Subst' (Src q) (Var q)
subst -> let ty :: Type (Origin (Src q)) (Name (Var q))
ty   = Subst' (Src q) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst Type (Origin (Src q)) (Name (Var q))
tvn
                         term :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
term = Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> TyTerm prim loc v
-> TyTerm prim loc v
-> TyTerm prim loc v
tyAppE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc (Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
f') (Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
a')
                     in  (Subst' (Src q) (Var q),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst' (Src q) (Var q)
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
term)

    (Subst' (Src q) (Var q),
 [(Type (Origin (Src q)) (Name (Var q)),
   TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
_               -> String -> InferOf q
forall a. HasCallStack => String -> a
error String
"Impossible has happened!"

inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam :: ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
x TermOf' q
body = do
  Name (Var q)
tvn <- InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
  (Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer (Name (Var q) -> ContextOf' q
ctx1 Name (Var q)
tvn) TermOf' q
body
  let ty :: Type (Origin (Src q)) (Name (Var q))
ty = Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v. loc -> Type loc v -> Type loc v -> Type loc v
arrowT Origin (Src q)
loc (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
phi (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc Name (Var q)
tvn)) (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm)
  (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
phi, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v
tyLamE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Name (Var q)
x TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm)
  where
    ctx1 :: Name (Var q) -> ContextOf' q
ctx1 Name (Var q)
tvn = Name (Var q)
-> Signature (Origin (Src q)) (Name (Var q))
-> ContextOf' q
-> ContextOf' q
forall v loc.
Ord v =>
v -> Signature loc v -> Context loc v -> Context loc v
insertCtx Name (Var q)
x (Origin (Src q)
-> Name (Var q) -> Signature (Origin (Src q)) (Name (Var q))
forall loc v. loc -> v -> Signature loc v
newVar Origin (Src q)
loc Name (Var q)
tvn) ContextOf' q
ctx

inferLet :: Lang q => ContextOf' q -> Origin (Src q) -> BindOf' q (TermOf' q) -> TermOf' q -> InferOf q
inferLet :: ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
inferLet ContextOf' q
ctx Origin (Src q)
loc BindOf' q (TermOf' q)
v TermOf' q
body = do
  (Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx (TermOf' q -> InferOf q) -> TermOf' q -> InferOf q
forall a b. (a -> b) -> a -> b
$ BindOf' q (TermOf' q) -> TermOf' q
forall loc var a. Bind loc var a -> a
bind'rhs BindOf' q (TermOf' q)
v
  let tBind :: Type (Origin (Src q)) (Name (Var q))
tBind = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm
  ContextOf' q
ctx1 <- [Bind
   (Origin (Src q))
   (Name (Var q))
   (Type (Origin (Src q)) (Name (Var q)))]
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall v loc.
IsVar v =>
[Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls [(TermOf' q -> Type (Origin (Src q)) (Name (Var q)))
-> BindOf' q (TermOf' q)
-> Bind
     (Origin (Src q))
     (Name (Var q))
     (Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type (Origin (Src q)) (Name (Var q))
-> TermOf' q -> Type (Origin (Src q)) (Name (Var q))
forall a b. a -> b -> a
const Type (Origin (Src q)) (Name (Var q))
tBind) BindOf' q (TermOf' q)
v] (Subst (Origin (Src q)) (Name (Var q))
-> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
phi ContextOf' q
ctx)
  (Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 TermOf' q
body
  let subst1 :: Subst (Origin (Src q)) (Name (Var q))
subst1 = Subst (Origin (Src q)) (Name (Var q))
phi Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
subst
      tyBind :: Bind
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
tyBind = BindOf' q (TermOf' q)
v { bind'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bind'rhs = Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm }
  (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return ( Subst (Origin (Src q)) (Name (Var q))
subst1
         , Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
 -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Bind
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> Bind loc v (TyTerm prim loc v)
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetE (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) Origin (Src q)
loc Bind
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
tyBind TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm
         )

inferLetRec :: forall q . Lang q
  => ContextOf' q -> Origin (Src q) -> [BindOf' q (TermOf' q)] -> TermOf' q
  -> InferOf q
inferLetRec :: ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
inferLetRec ContextOf' q
ctx Origin (Src q)
topLoc [BindOf' q (TermOf' q)]
vs TermOf' q
body = do
  [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx <- [BindOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
getTypesLhs [BindOf' q (TermOf' q)]
vs
  (Subst (Origin (Src q)) (Name (Var q))
phi, [(Type' (Src q) (Var q),
  TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
rhsTyTerms) <- ContextOf' q
-> [TermOf' q]
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      [(Type' (Src q) (Var q),
        TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms (ContextOf' q
ctx ContextOf' q -> ContextOf' q -> ContextOf' q
forall a. Semigroup a => a -> a -> a
<> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> ContextOf' q
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx) Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a. Monoid a => a
mempty) [TermOf' q]
exprBinds
  let ([Type' (Src q) (Var q)]
tBinds, [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
bindsTyTerms) = [(Type' (Src q) (Var q),
  TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> ([Type' (Src q) (Var q)],
    [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type' (Src q) (Var q),
  TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
rhsTyTerms
  case ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> [Type' (Src q) (Var q)]
-> Either
     (TypeError (Src q) (Name (Var q)))
     (ContextOf' q,
      [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))],
      Subst (Origin (Src q)) (Name (Var q)))
forall v (f :: * -> * -> *) loc a.
(CanApply f, IsVar v, Show loc) =>
f (Origin loc) (Name v)
-> [(a, Signature (Origin loc) (Name v))]
-> Subst (Origin loc) (Name v)
-> [Type' loc v]
-> Either
     (TypeError loc (Name v))
     (f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
      Subst (Origin loc) (Name v))
unifyRhs ContextOf' q
ctx [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx Subst (Origin (Src q)) (Name (Var q))
phi [Type' (Src q) (Var q)]
tBinds of
    Right (ContextOf' q
ctx1, [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx1, Subst (Origin (Src q)) (Name (Var q))
subst) -> [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> TermOf' q
-> InferOf q
inferBody [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
bindsTyTerms ContextOf' q
ctx1 [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx1 Subst (Origin (Src q)) (Name (Var q))
subst TermOf' q
body
    Left TypeError (Src q) (Name (Var q))
err                     -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
topLoc
  where
    exprBinds :: [TermOf' q]
exprBinds = (BindOf' q (TermOf' q) -> TermOf' q)
-> [BindOf' q (TermOf' q)] -> [TermOf' q]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindOf' q (TermOf' q) -> TermOf' q
forall loc var a. Bind loc var a -> a
bind'rhs [BindOf' q (TermOf' q)]
vs
    locBinds :: [Origin (Src q)]
locBinds  = (BindOf' q (TermOf' q) -> Origin (Src q))
-> [BindOf' q (TermOf' q)] -> [Origin (Src q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindOf' q (TermOf' q) -> Origin (Src q)
forall loc var a. Bind loc var a -> loc
bind'loc [BindOf' q (TermOf' q)]
vs

    getTypesLhs :: [BindOf' q (TermOf' q)] -> InferM (Src q) (Var q) [(Name (Var q), SignatureOf' q)]
    getTypesLhs :: [BindOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
getTypesLhs [BindOf' q (TermOf' q)]
lhs = (BindOf' q (TermOf' q)
 -> InferM
      (Src q)
      (Var q)
      (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> [BindOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\BindOf' q (TermOf' q)
b -> (Name (Var q)
 -> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM
     (Src q)
     (Var q)
     (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BindOf' q (TermOf' q) -> Name (Var q)
forall loc var a. Bind loc var a -> var
bind'lhs BindOf' q (TermOf' q)
b, ) (Signature (Origin (Src q)) (Name (Var q))
 -> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> (Name (Var q) -> Signature (Origin (Src q)) (Name (Var q)))
-> Name (Var q)
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Origin (Src q)
-> Name (Var q) -> Signature (Origin (Src q)) (Name (Var q))
forall loc v. loc -> v -> Signature loc v
newVar (BindOf' q (TermOf' q) -> Origin (Src q)
forall loc var a. Bind loc var a -> loc
bind'loc BindOf' q (TermOf' q)
b)) InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar) [BindOf' q (TermOf' q)]
lhs

    unifyRhs :: f (Origin loc) (Name v)
-> [(a, Signature (Origin loc) (Name v))]
-> Subst (Origin loc) (Name v)
-> [Type' loc v]
-> Either
     (TypeError loc (Name v))
     (f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
      Subst (Origin loc) (Name v))
unifyRhs f (Origin loc) (Name v)
context [(a, Signature (Origin loc) (Name v))]
lhsCtx Subst (Origin loc) (Name v)
phi [Type' loc v]
tBinds =
      (Subst (Origin loc) (Name v)
 -> (f (Origin loc) (Name v),
     [(a, Signature (Origin loc) (Name v))],
     Subst (Origin loc) (Name v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc (Name v))
     (f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
      Subst (Origin loc) (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Subst (Origin loc) (Name v)
subst -> (f (Origin loc) (Name v)
context1, [(a, Signature (Origin loc) (Name v))]
lhsCtx1, Subst (Origin loc) (Name v)
subst)) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
 -> Either
      (TypeError loc (Name v))
      (f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
       Subst (Origin loc) (Name v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc (Name v))
     (f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
      Subst (Origin loc) (Name v))
forall a b. (a -> b) -> a -> b
$ Subst (Origin loc) (Name v)
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst (Origin loc) (Name v)
phi [Type' loc v]
ts [Type' loc v]
tBinds
      where
        context1 :: f (Origin loc) (Name v)
context1 = Subst (Origin loc) (Name v)
-> f (Origin loc) (Name v) -> f (Origin loc) (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
phi f (Origin loc) (Name v)
context
        lhsCtx1 :: [(a, Signature (Origin loc) (Name v))]
lhsCtx1  = ((a, Signature (Origin loc) (Name v))
 -> (a, Signature (Origin loc) (Name v)))
-> [(a, Signature (Origin loc) (Name v))]
-> [(a, Signature (Origin loc) (Name v))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Signature (Origin loc) (Name v)
 -> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Signature (Origin loc) (Name v)
  -> Signature (Origin loc) (Name v))
 -> (a, Signature (Origin loc) (Name v))
 -> (a, Signature (Origin loc) (Name v)))
-> (Signature (Origin loc) (Name v)
    -> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
forall a b. (a -> b) -> a -> b
$ Subst (Origin loc) (Name v)
-> Signature (Origin loc) (Name v)
-> Signature (Origin loc) (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
phi) [(a, Signature (Origin loc) (Name v))]
lhsCtx
        ts :: [Type' loc v]
ts = ((a, Signature (Origin loc) (Name v)) -> Type' loc v)
-> [(a, Signature (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Signature (Origin loc) (Name v) -> Type' loc v
forall loc var. Signature loc var -> Type loc var
oldBvar (Signature (Origin loc) (Name v) -> Type' loc v)
-> ((a, Signature (Origin loc) (Name v))
    -> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> Type' loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Signature (Origin loc) (Name v))
-> Signature (Origin loc) (Name v)
forall a b. (a, b) -> b
snd) [(a, Signature (Origin loc) (Name v))]
lhsCtx1

    oldBvar :: Signature loc var -> Type loc var
oldBvar = (SignatureF loc var (Type loc var) -> Type loc var)
-> Fix (SignatureF loc var) -> Type loc var
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix SignatureF loc var (Type loc var) -> Type loc var
forall loc var. SignatureF loc var (Type loc var) -> Type loc var
go (Fix (SignatureF loc var) -> Type loc var)
-> (Signature loc var -> Fix (SignatureF loc var))
-> Signature loc var
-> Type loc var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature loc var -> Fix (SignatureF loc var)
forall loc var. Signature loc var -> Fix (SignatureF loc var)
unSignature
      where
        go :: SignatureF loc var (Type loc var) -> Type loc var
go  = \case
          MonoT Type loc var
t       -> Type loc var
t
          ForAllT loc
_ var
_ Type loc var
t -> Type loc var
t

    inferBody :: [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> TermOf' q
-> InferOf q
inferBody [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
termBinds ContextOf' q
context [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx Subst (Origin (Src q)) (Name (Var q))
subst TermOf' q
expr = do
      ContextOf' q
ctx1 <- [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall v loc.
IsVar v =>
[Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls ((Origin (Src q)
 -> (Name (Var q), Type' (Src q) (Var q))
 -> Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q)))
-> [Origin (Src q)]
-> [(Name (Var q), Type' (Src q) (Var q))]
-> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Origin (Src q)
loc (Name (Var q)
v, Type' (Src q) (Var q)
ty) -> Origin (Src q)
-> Name (Var q)
-> Type' (Src q) (Var q)
-> Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))
forall loc var a. loc -> var -> a -> Bind loc var a
Bind Origin (Src q)
loc Name (Var q)
v Type' (Src q) (Var q)
ty) [Origin (Src q)]
locBinds ([(Name (Var q), Type' (Src q) (Var q))]
 -> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))])
-> [(Name (Var q), Type' (Src q) (Var q))]
-> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
forall a b. (a -> b) -> a -> b
$ ((Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
 -> (Name (Var q), Type' (Src q) (Var q)))
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> [(Name (Var q), Type' (Src q) (Var q))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Signature (Origin (Src q)) (Name (Var q))
 -> Type' (Src q) (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Signature (Origin (Src q)) (Name (Var q))
  -> Type' (Src q) (Var q))
 -> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
 -> (Name (Var q), Type' (Src q) (Var q)))
-> (Signature (Origin (Src q)) (Name (Var q))
    -> Type' (Src q) (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q))
forall a b. (a -> b) -> a -> b
$ Signature (Origin (Src q)) (Name (Var q)) -> Type' (Src q) (Var q)
forall loc var. Signature loc var -> Type loc var
oldBvar (Signature (Origin (Src q)) (Name (Var q))
 -> Type' (Src q) (Var q))
-> (Signature (Origin (Src q)) (Name (Var q))
    -> Signature (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst) [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx) (ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q))
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst ContextOf' q
context
      (Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 TermOf' q
expr
      let tyBinds :: [Bind
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyBinds = (BindOf' q (TermOf' q)
 -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
 -> Bind
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> [BindOf' q (TermOf' q)]
-> [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> [Bind
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BindOf' q (TermOf' q)
bind TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhs -> BindOf' q (TermOf' q)
bind { bind'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bind'rhs = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhs }) [BindOf' q (TermOf' q)]
vs [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
termBinds
      (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
subst Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
phi, Type' (Src q) (Var q)
-> Origin (Src q)
-> [Bind
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> [Bind loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetRecE (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q)
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) Origin (Src q)
topLoc [Bind
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyBinds TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm)

inferAssertType :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType :: ContextOf' q
-> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType ContextOf' q
ctx Origin (Src q)
loc TermOf' q
a TypeOf' q
ty = do
  (Subst' (Src q) (Var q)
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
a
  case Subst' (Src q) (Var q)
-> TypeOf' q
-> TypeOf' q
-> Either
     (TypeError (Src q) (Name (Var q))) (Subst' (Src q) (Var q))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' (Src q) (Var q)
phi TypeOf' q
ty (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)) -> TypeOf' q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm) of
    Right Subst' (Src q) (Var q)
subst -> do
      let subst' :: Subst' (Src q) (Var q)
subst' = Subst' (Src q) (Var q)
phi Subst' (Src q) (Var q)
-> Subst' (Src q) (Var q) -> Subst' (Src q) (Var q)
forall a. Semigroup a => a -> a -> a
<> Subst' (Src q) (Var q)
subst
      (Subst' (Src q) (Var q),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst' (Src q) (Var q)
subst', Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst' (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
 -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TypeOf' q
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc prim v.
loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v
tyAssertTypeE Origin (Src q)
loc TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm TypeOf' q
ty)
    Left TypeError (Src q) (Name (Var q))
err -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc

inferConstr :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr :: ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
tag = do
  case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx Name (Var q)
tag ContextOf' q
ctx of
    Just Signature (Origin (Src q)) (Name (Var q))
ty -> do
      Type (Origin (Src q)) (Name (Var q))
vT <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance Signature (Origin (Src q)) (Name (Var q))
ty
      (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim. loc -> Type loc v -> v -> TyTerm prim loc v
tyConstrE Origin (Src q)
loc Type (Origin (Src q)) (Name (Var q))
vT Name (Var q)
tag)
    Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Name (Var q)
tag) Origin (Src q)
loc

inferCase :: forall q . Lang q
  => ContextOf' q -> Origin (Src q) -> TermOf' q -> [CaseAltOf' q (TermOf' q)]
  -> InferOf q
inferCase :: ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
inferCase ContextOf' q
ctx Origin (Src q)
loc TermOf' q
e [CaseAltOf' q (TermOf' q)]
caseAlts = do
  (Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
e
  Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
mAlts <- Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         [CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
inferAlts Subst (Origin (Src q)) (Name (Var q))
phi (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) ([CaseAltOf' q (TermOf' q)]
 -> InferM
      (Src q)
      (Var q)
      (Maybe
         (Subst (Origin (Src q)) (Name (Var q)),
          Type (Origin (Src q)) (Name (Var q)),
          [CaseAlt
             (Origin (Src q))
             (Name (Var q))
             (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         [CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall a b. (a -> b) -> a -> b
$ [CaseAltOf' q (TermOf' q)]
caseAlts
  case Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
mAlts of
    Just (Subst (Origin (Src q)) (Name (Var q))
psi, Type (Origin (Src q)) (Name (Var q))
tRes, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyAlts) -> (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return ( Subst (Origin (Src q)) (Name (Var q))
psi
                                       , Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
psi (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
 -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> TyTerm prim loc v
-> [CaseAlt loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
tyCaseE Type (Origin (Src q)) (Name (Var q))
tRes Origin (Src q)
loc (Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
psi TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyAlts)
    Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
Nothing -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> TypeError loc var
EmptyCaseExpr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc)) Origin (Src q)
loc
  where
    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)]))
    inferAlts :: Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         [CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
inferAlts Subst (Origin (Src q)) (Name (Var q))
substE Type (Origin (Src q)) (Name (Var q))
tE [CaseAltOf' q (TermOf' q)]
alts = do
      (Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
_, Maybe (Type (Origin (Src q)) (Name (Var q)))
mTRes, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
as) <- ((Subst (Origin (Src q)) (Name (Var q)),
  Type (Origin (Src q)) (Name (Var q)),
  Maybe (Type (Origin (Src q)) (Name (Var q))),
  [CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
 -> CaseAltOf' q (TermOf' q)
 -> InferM
      (Src q)
      (Var q)
      (Subst (Origin (Src q)) (Name (Var q)),
       Type (Origin (Src q)) (Name (Var q)),
       Maybe (Type (Origin (Src q)) (Name (Var q))),
       [CaseAlt
          (Origin (Src q))
          (Name (Var q))
          (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
-> (Subst (Origin (Src q)) (Name (Var q)),
    Type (Origin (Src q)) (Name (Var q)),
    Maybe (Type (Origin (Src q)) (Name (Var q))),
    [CaseAlt
       (Origin (Src q))
       (Name (Var q))
       (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> [CaseAltOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
go (Subst (Origin (Src q)) (Name (Var q))
substE, Type (Origin (Src q)) (Name (Var q))
tE, Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. Maybe a
Nothing, []) [CaseAltOf' q (TermOf' q)]
alts
      Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         [CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
   (Subst (Origin (Src q)) (Name (Var q)),
    Type (Origin (Src q)) (Name (Var q)),
    [CaseAlt
       (Origin (Src q))
       (Name (Var q))
       (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
 -> InferM
      (Src q)
      (Var q)
      (Maybe
         (Subst (Origin (Src q)) (Name (Var q)),
          Type (Origin (Src q)) (Name (Var q)),
          [CaseAlt
             (Origin (Src q))
             (Name (Var q))
             (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])))
-> Maybe
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         [CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall a b. (a -> b) -> a -> b
$ case Maybe (Type (Origin (Src q)) (Name (Var q)))
mTRes of
        Just Type (Origin (Src q)) (Name (Var q))
tRes -> (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> Maybe
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall a. a -> Maybe a
Just (Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
tRes, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. [a] -> [a]
L.reverse [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
as)
        Maybe (Type (Origin (Src q)) (Name (Var q)))
Nothing   -> Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall a. Maybe a
Nothing
      where
        go :: (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
go initSt :: (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt@(Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
tyTop, Maybe (Type (Origin (Src q)) (Name (Var q)))
mTyPrevRhs, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res) CaseAltOf' q (TermOf' q)
alt = do
          Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
mRes <- CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         CaseAlt
           (Origin (Src q))
           (Name (Var q))
           (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
inferAlt (Subst (Origin (Src q)) (Name (Var q))
-> CaseAltOf' q (TermOf' q) -> CaseAltOf' q (TermOf' q)
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst CaseAltOf' q (TermOf' q)
alt)
          case Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
mRes of
            Just (Subst (Origin (Src q)) (Name (Var q))
phi, Type (Origin (Src q)) (Name (Var q))
tyRhs, Type (Origin (Src q)) (Name (Var q))
tResExpected, CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1) -> do
              let subst1 :: Subst (Origin (Src q)) (Name (Var q))
subst1 = Subst (Origin (Src q)) (Name (Var q))
subst Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
phi
              case Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
     (TypeError (Src q) (Name (Var q)))
     (Subst (Origin (Src q)) (Name (Var q)))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin (Src q)) (Name (Var q))
subst1 (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 Type (Origin (Src q)) (Name (Var q))
tyTop) (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 Type (Origin (Src q)) (Name (Var q))
tResExpected) of
                Right Subst (Origin (Src q)) (Name (Var q))
subst2 -> do
                  case Maybe (Type (Origin (Src q)) (Name (Var q)))
mTyPrevRhs of
                    Maybe (Type (Origin (Src q)) (Name (Var q)))
Nothing -> (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q))
subst2, Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyTop, Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. a -> Maybe a
Just (Type (Origin (Src q)) (Name (Var q))
 -> Maybe (Type (Origin (Src q)) (Name (Var q))))
-> Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyRhs, Subst (Origin (Src q)) (Name (Var q))
-> CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst2 CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1 CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. a -> [a] -> [a]
: [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res)
                    Just Type (Origin (Src q)) (Name (Var q))
tyPrevRhs -> do
                      case Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
     (TypeError (Src q) (Name (Var q)))
     (Subst (Origin (Src q)) (Name (Var q)))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin (Src q)) (Name (Var q))
subst2 (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyRhs) (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyPrevRhs) of
                        Right Subst (Origin (Src q)) (Name (Var q))
subst3 -> (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q))
subst3, Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst3 Type (Origin (Src q)) (Name (Var q))
tyTop, Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. a -> Maybe a
Just (Type (Origin (Src q)) (Name (Var q))
 -> Maybe (Type (Origin (Src q)) (Name (Var q))))
-> Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst3 Type (Origin (Src q)) (Name (Var q))
tyRhs, Subst (Origin (Src q)) (Name (Var q))
-> CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst3 CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1 CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. a -> [a] -> [a]
: [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res)
                        Left TypeError (Src q) (Name (Var q))
err     -> do
                          [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
                          (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt
                Left TypeError (Src q) (Name (Var q))
err     -> do
                  [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
                  (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt
            Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
Nothing -> do
              [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin (Origin (Src q) -> Src q) -> Origin (Src q) -> Src q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Origin (Src q)
forall loc v a. CaseAlt loc v a -> loc
caseAlt'loc CaseAltOf' q (TermOf' q)
alt) (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt)]
              (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
     (Src q)
     (Var q)
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Maybe (Type (Origin (Src q)) (Name (Var q))),
      [CaseAlt
         (Origin (Src q))
         (Name (Var q))
         (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Maybe (Type (Origin (Src q)) (Name (Var q))),
 [CaseAlt
    (Origin (Src q))
    (Name (Var q))
    (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt

    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q)))
    inferAlt :: CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         CaseAlt
           (Origin (Src q))
           (Name (Var q))
           (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
inferAlt CaseAltOf' q (TermOf' q)
alt =
      case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt) ContextOf' q
ctx of
        Just Signature (Origin (Src q)) (Name (Var q))
ctxConTy -> do
          Type (Origin (Src q)) (Name (Var q))
conTy <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance Signature (Origin (Src q)) (Name (Var q))
ctxConTy
          let ([Type (Origin (Src q)) (Name (Var q))]
tyArgs, Type (Origin (Src q)) (Name (Var q))
tyRes) = Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
    Type (Origin (Src q)) (Name (Var q)))
splitFunT Type (Origin (Src q)) (Name (Var q))
conTy
              expectedArity :: Int
expectedArity = [Type (Origin (Src q)) (Name (Var q))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type (Origin (Src q)) (Name (Var q))]
tyArgs
              actualArity :: Int
actualArity   = [(Origin (Src q), Name (Var q))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Origin (Src q), Name (Var q))] -> Int)
-> [(Origin (Src q), Name (Var q))] -> Int
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> [(Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt
          Bool -> InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
expectedArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
actualArity) (InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ())
-> InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ()
forall a b. (a -> b) -> a -> b
$ [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Src q
-> Name (Var q) -> Int -> Int -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> Int -> Int -> TypeError loc var
ConsArityMismatch (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin (Origin (Src q) -> Src q) -> Origin (Src q) -> Src q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Origin (Src q)
forall loc v a. CaseAlt loc v a -> loc
caseAlt'loc CaseAltOf' q (TermOf' q)
alt) (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt) Int
expectedArity Int
actualArity]
          let argVars :: [(Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars = (Type (Origin (Src q)) (Name (Var q))
 -> (Origin (Src q), Name (Var q))
 -> (Name (Var q),
     (Origin (Src q), Type (Origin (Src q)) (Name (Var q)))))
-> [Type (Origin (Src q)) (Name (Var q))]
-> [(Origin (Src q), Name (Var q))]
-> [(Name (Var q),
     (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Type (Origin (Src q)) (Name (Var q))
ty (Origin (Src q)
src, Name (Var q)
arg) -> (Name (Var q)
arg, (Origin (Src q)
src, Type (Origin (Src q)) (Name (Var q))
ty))) [Type (Origin (Src q)) (Name (Var q))]
tyArgs (CaseAltOf' q (TermOf' q) -> [(Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt)
              ctx1 :: ContextOf' q
ctx1 = Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> ContextOf' q
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
 -> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q))))
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ ((Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
 -> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> [(Name (Var q),
     (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
 -> Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q),
    (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
  -> Signature (Origin (Src q)) (Name (Var q)))
 -> (Name (Var q),
     (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
 -> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> ((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
    -> Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q),
    (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall loc src. Type loc src -> Signature loc src
monoT (Type (Origin (Src q)) (Name (Var q))
 -> Signature (Origin (Src q)) (Name (Var q)))
-> ((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
    -> Type (Origin (Src q)) (Name (Var q)))
-> (Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q))
forall a b. (a, b) -> b
snd) [(Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars) Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a. Monoid a => a
mempty ContextOf' q -> ContextOf' q -> ContextOf' q
forall a. Semigroup a => a -> a -> a
<> ContextOf' q
ctx
          (Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 (TermOf' q -> InferOf q) -> TermOf' q -> InferOf q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> TermOf' q
forall loc v a. CaseAlt loc v a -> a
caseAlt'rhs CaseAltOf' q (TermOf' q)
alt
          let alt' :: CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt' = CaseAltOf' q (TermOf' q)
alt { caseAlt'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
caseAlt'rhs = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs }
          Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         CaseAlt
           (Origin (Src q))
           (Name (Var q))
           (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe
   (Subst (Origin (Src q)) (Name (Var q)),
    Type (Origin (Src q)) (Name (Var q)),
    Type (Origin (Src q)) (Name (Var q)),
    CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
 -> InferM
      (Src q)
      (Var q)
      (Maybe
         (Subst (Origin (Src q)) (Name (Var q)),
          Type (Origin (Src q)) (Name (Var q)),
          Type (Origin (Src q)) (Name (Var q)),
          CaseAlt
            (Origin (Src q))
            (Name (Var q))
            (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))))
-> Maybe
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      CaseAlt
        (Origin (Src q))
        (Name (Var q))
        (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         CaseAlt
           (Origin (Src q))
           (Name (Var q))
           (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall a b. (a -> b) -> a -> b
$ (Subst (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 Type (Origin (Src q)) (Name (Var q)),
 CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> Maybe
     (Subst (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      Type (Origin (Src q)) (Name (Var q)),
      CaseAlt
        (Origin (Src q))
        (Name (Var q))
        (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
forall a. a -> Maybe a
Just (Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs, Type (Origin (Src q)) (Name (Var q))
tyRes, CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt')
        Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing -> Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
     (Src q)
     (Var q)
     (Maybe
        (Subst (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         Type (Origin (Src q)) (Name (Var q)),
         CaseAlt
           (Origin (Src q))
           (Name (Var q))
           (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  (Subst (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   Type (Origin (Src q)) (Name (Var q)),
   CaseAlt
     (Origin (Src q))
     (Name (Var q))
     (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
forall a. Maybe a
Nothing

    splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)
    splitFunT :: Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
    Type (Origin (Src q)) (Name (Var q)))
splitFunT Type (Origin (Src q)) (Name (Var q))
arrT = [Type (Origin (Src q)) (Name (Var q))]
-> Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
    Type (Origin (Src q)) (Name (Var q)))
forall loc var.
[Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go [] Type (Origin (Src q)) (Name (Var q))
arrT
      where
        go :: [Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go [Type loc var]
argsT (Type (Fix TypeF loc var (Fix (TypeF loc var))
t)) = case TypeF loc var (Fix (TypeF loc var))
t of
          ArrowT loc
_loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b -> [Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go (Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF loc var)
a Type loc var -> [Type loc var] -> [Type loc var]
forall a. a -> [a] -> [a]
: [Type loc var]
argsT) (Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF loc var)
b)
          TypeF loc var (Fix (TypeF loc var))
other           -> ([Type loc var] -> [Type loc var]
forall a. [a] -> [a]
reverse [Type loc var]
argsT, Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF loc var) -> Type loc var)
-> Fix (TypeF loc var) -> Type loc var
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF loc var (Fix (TypeF loc var))
other)

    applyAlt :: Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst loc v
subst CaseAlt loc v (f loc v)
alt = CaseAlt loc v (f loc v)
alt { caseAlt'rhs :: f loc v
caseAlt'rhs = Subst loc v -> f loc v -> f loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
subst (f loc v -> f loc v) -> f loc v -> f loc v
forall a b. (a -> b) -> a -> b
$ CaseAlt loc v (f loc v) -> f loc v
forall loc v a. CaseAlt loc v a -> a
caseAlt'rhs CaseAlt loc v (f loc v)
alt }


inferBottom :: Lang q => Origin (Src q) -> InferOf q
inferBottom :: Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc = do
  Type (Origin (Src q)) (Name (Var q))
ty <- (Name (Var q) -> Type (Origin (Src q)) (Name (Var q)))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc) InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
  (Subst (Origin (Src q)) (Name (Var q)),
 TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim. Type loc v -> loc -> TyTerm prim loc v
tyBottomE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc)

newInstance :: IsVar v => Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance :: Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance = ((Subst loc (Name v), Type loc (Name v)) -> Type loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Type loc (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Subst loc (Name v) -> Type loc (Name v) -> Type loc (Name v))
-> (Subst loc (Name v), Type loc (Name v)) -> Type loc (Name v)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Subst loc (Name v) -> Type loc (Name v) -> Type loc (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply) (InferM loc' v (Subst loc (Name v), Type loc (Name v))
 -> InferM loc' v (Type loc (Name v)))
-> (Signature loc (Name v)
    -> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> Signature loc (Name v)
-> InferM loc' v (Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
 -> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> Fix (SignatureF loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall loc loc.
SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
go (Fix (SignatureF loc (Name v))
 -> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> (Signature loc (Name v) -> Fix (SignatureF loc (Name v)))
-> Signature loc (Name v)
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature loc (Name v) -> Fix (SignatureF loc (Name v))
forall loc var. Signature loc var -> Fix (SignatureF loc var)
unSignature
  where
    go :: SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
go = \case
      MonoT Type loc (Name v)
ty -> (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst loc (Name v)
forall a. Monoid a => a
mempty, Type loc (Name v)
ty)
      ForAllT loc
loc Name v
v (Subst Map (Name v) (Type loc (Name v))
m, Type loc (Name v)
ty) -> (Name v -> (Subst loc (Name v), Type loc (Name v)))
-> InferM loc v (Name v)
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name v
nv -> (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v))
-> Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall a b. (a -> b) -> a -> b
$ Name v
-> Type loc (Name v)
-> Map (Name v) (Type loc (Name v))
-> Map (Name v) (Type loc (Name v))
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name v
v (loc -> Name v -> Type loc (Name v)
forall loc var. loc -> var -> Type loc var
varT loc
loc Name v
nv) Map (Name v) (Type loc (Name v))
m, Type loc (Name v)
ty)) InferM loc v (Name v)
forall v loc. IsVar v => InferM loc v (Name v)
freshVar

newVar :: loc -> v -> Signature loc v
newVar :: loc -> v -> Signature loc v
newVar loc
loc v
tvn = Type loc v -> Signature loc v
forall loc src. Type loc src -> Signature loc src
monoT (Type loc v -> Signature loc v) -> Type loc v -> Signature loc v
forall a b. (a -> b) -> a -> b
$ loc -> v -> Type loc v
forall loc var. loc -> var -> Type loc var
varT loc
loc v
tvn

freshVar :: IsVar v => InferM loc v (Name v)
freshVar :: InferM loc v (Name v)
freshVar = do
  Int
n <- InferM loc v Int
forall s (m :: * -> *). MonadState s m => m s
get
  Int -> InferM loc v ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> InferM loc v ()) -> Int -> InferM loc v ()
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  Name v -> InferM loc v (Name v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name v -> InferM loc v (Name v))
-> Name v -> InferM loc v (Name v)
forall a b. (a -> b) -> a -> b
$ Int -> Name v
forall v. Int -> Name v
FreshName Int
n

inferTerms :: Lang q
  => ContextOf' q
  -> [TermOf' q]
  -> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms :: ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms ContextOf' q
ctx [TermOf' q]
ts = case [TermOf' q]
ts of
  []   -> (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((SubstOf' q, [(TypeOf' q, TyTermOf' q)])
 -> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)]))
-> (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall a b. (a -> b) -> a -> b
$ (SubstOf' q
forall a. Monoid a => a
mempty, [])
  TermOf' q
a:[TermOf' q]
as -> do
    (SubstOf' q
phi, TyTermOf' q
termA) <- ContextOf' q
-> TermOf' q -> InferM (Src q) (Var q) (SubstOf' q, TyTermOf' q)
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
a
    let ta :: TypeOf' q
ta = TyTermOf' q -> TypeOf' q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTermOf' q
termA
    (SubstOf' q
psi, [(TypeOf' q, TyTermOf' q)]
tas) <- ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms (SubstOf' q -> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
phi ContextOf' q
ctx) [TermOf' q]
as
    (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall (m :: * -> *) a. Monad m => a -> m a
return ( SubstOf' q
phi SubstOf' q -> SubstOf' q -> SubstOf' q
forall a. Semigroup a => a -> a -> a
<> SubstOf' q
psi
           , (SubstOf' q -> TypeOf' q -> TypeOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
psi TypeOf' q
ta, SubstOf' q -> TyTermOf' q -> TyTermOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
psi TyTermOf' q
termA) (TypeOf' q, TyTermOf' q)
-> [(TypeOf' q, TyTermOf' q)] -> [(TypeOf' q, TyTermOf' q)]
forall a. a -> [a] -> [a]
: [(TypeOf' q, TyTermOf' q)]
tas
           )

-- | Unification function. Checks weather two types unify.
-- First argument is current substitution.
unify :: (IsVar v, Show loc)
  => Subst' loc v
  -> Type' loc v
  -> Type' loc v
  -> Either (TypeError loc (Name v)) (Subst' loc v)
unify :: Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x)) (Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y)) = {- trace (unlines ["UNIFY", ppShow tx, ppShow ty]) $ -}
  case (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y) of
    (VarT Origin loc
loc Name v
tvn, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
t) ->
        let phiTvn :: Type' loc v
phiTvn = Subst' loc v -> Origin loc -> Name v -> Type' loc v
forall v loc.
IsVar v =>
Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar Subst' loc v
phi Origin loc
loc Name v
tvn
            phiT :: Type' loc v
phiT   = Subst' loc v -> Type' loc v -> Type' loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
t))
        in  if Type' loc v
phiTvn Type' loc v -> Type' loc v -> Bool
forall v loc. Eq v => Type loc v -> Type loc v -> Bool
`eqIgnoreLoc` Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
tvn
              then Subst' loc v
-> Origin loc
-> Name v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v
-> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend Subst' loc v
phi Origin loc
loc Name v
tvn Type' loc v
phiT
              else Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi Type' loc v
phiTvn Type' loc v
phiT
    (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a, VarT Origin loc
locB Name v
v) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
locB Name v
v) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a) -- (conT locA name $ fmap Type ts)
    (ConT Origin loc
locA Name v
n [Fix (TypeF (Origin loc) (Name v))]
xs, ConT Origin loc
locB Name v
m [Fix (TypeF (Origin loc) (Name v))]
ys) ->
      if Name v
n Name v -> Name v -> Bool
forall a. Eq a => a -> a -> Bool
== Name v
m
        then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
        else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB
    (ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a1 Fix (TypeF (Origin loc) (Name v))
a2, ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b1 Fix (TypeF (Origin loc) (Name v))
b2) -> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
a1, Fix (TypeF (Origin loc) (Name v))
a2]) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
b1, Fix (TypeF (Origin loc) (Name v))
b2])
    (TupleT Origin loc
locA [Fix (TypeF (Origin loc) (Name v))]
xs, TupleT Origin loc
locB [Fix (TypeF (Origin loc) (Name v))]
ys) ->
      if [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
ys
        then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
        else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB
    (ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a, ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
a) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
b)
    (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
b) -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc (Type' loc v -> Loc (Type' loc v))
-> Type' loc v -> Loc (Type' loc v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a) (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc (Type' loc v -> Loc (Type' loc v))
-> Type' loc v -> Loc (Type' loc v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
b)
  where
    unifyErr :: Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB = TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError loc (Name v)
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$
      loc
-> Type loc (Name v) -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr (Origin loc -> Origin loc -> loc
forall a. Show a => Origin a -> Origin a -> a
chooseUserOrigin Origin loc
locA Origin loc
locB)
               ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin (Type' loc v -> Type loc (Name v))
-> Type' loc v -> Type loc (Name v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x))
               ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin (Type' loc v -> Type loc (Name v))
-> Type' loc v -> Type loc (Name v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y))

eqIgnoreLoc :: Eq v => Type loc v -> Type loc v -> Bool
eqIgnoreLoc :: Type loc v -> Type loc v -> Bool
eqIgnoreLoc = Type () v -> Type () v -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Type () v -> Type () v -> Bool)
-> (Type loc v -> Type () v) -> Type loc v -> Type loc v -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (loc -> ()) -> Type loc v -> Type () v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc (() -> loc -> ()
forall a b. a -> b -> a
const ())

applyVar :: IsVar v => Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar :: Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar (Subst Map (Name v) (Type' loc v)
subst) Origin loc
loc Name v
v = Type' loc v -> Maybe (Type' loc v) -> Type' loc v
forall a. a -> Maybe a -> a
fromMaybe (Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
v) (Maybe (Type' loc v) -> Type' loc v)
-> Maybe (Type' loc v) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ Name v -> Map (Name v) (Type' loc v) -> Maybe (Type' loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name v
v Map (Name v) (Type' loc v)
subst

extend
  :: (IsVar v, MonadError (TypeError loc (Name v)) m)
  => Subst' loc v -> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend :: Subst' loc v
-> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend Subst' loc v
phi Origin loc
loc Name v
tvn Type' loc v
ty
  | Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
tvn Type' loc v -> Type' loc v -> Bool
forall v loc. Eq v => Type loc v -> Type loc v -> Bool
`eqIgnoreLoc` Type' loc v
ty = Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
phi
  | Name v -> VarSet (Origin loc) (Name v) -> Bool
forall var src. Ord var => var -> VarSet src var -> Bool
memberVarSet Name v
tvn (Type' loc v -> VarSet (Origin loc) (Name v)
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type' loc v
ty)  = TypeError loc (Name v) -> m (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError loc (Name v) -> m (Subst' loc v))
-> TypeError loc (Name v) -> m (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ loc -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr (Origin loc -> loc
forall a. Origin a -> a
fromOrigin Origin loc
loc) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
ty)
  | Bool
otherwise                     = Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst' loc v -> m (Subst' loc v))
-> Subst' loc v -> m (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ Subst' loc v
phi Subst' loc v -> Subst' loc v -> Subst' loc v
forall a. Semigroup a => a -> a -> a
<> Name v -> Type' loc v -> Subst' loc v
forall v loc. v -> Type loc v -> Subst loc v
delta Name v
tvn Type' loc v
ty

unifyl :: (IsVar v, Show loc)
  => Subst' loc v
  -> [Type' loc v]
  -> [Type' loc v]
  -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl :: Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
 -> Either (TypeError loc (Name v)) (Subst' loc v)
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
(Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)]
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ [Type' loc v] -> [Type' loc v] -> [(Type' loc v, Type' loc v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type' loc v]
as [Type' loc v]
bs
  where
    go :: (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) Either (TypeError loc (Name v)) (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either (TypeError loc (Name v)) (Subst' loc v)
eSubst

-- | Checks if first argument one type is subtype of the second one.
subtypeOf :: (IsVar v, Show loc, Eq loc)
  => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
subtypeOf :: Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
subtypeOf Type loc v
a Type loc v
b =
  Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
 -> Either (TypeError loc v) (Subst loc v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ (TypeError loc (Name v) -> TypeError loc v)
-> (Subst (Origin loc) (Name v)
    -> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeError loc (Name v) -> TypeError loc v
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError loc (Name v) -> TypeError loc v)
-> (TypeError loc (Name v) -> TypeError loc (Name v))
-> TypeError loc (Name v)
-> TypeError loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError loc (Name v) -> TypeError loc (Name v)
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
forall v loc.
Ord v =>
Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v))
-> (Subst (Origin loc) (Name v) -> Subst loc (Name v))
-> Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) (Name v) -> Subst loc (Name v)
forall v loc. Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
 -> Either
      (TypeError loc v) (Either (TypeError loc v) (Subst loc v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall a b. (a -> b) -> a -> b
$
    Subst (Origin loc) (Name v)
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst (Origin loc) (Name v)
forall a. Monoid a => a
mempty ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
Proven Type loc v
a) ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode Type loc v
b)

genSubtypeOf :: (IsVar v, Show loc)
  => Subst' loc v
  -> Type' loc v
  -> Type' loc v
  -> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf :: Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
phi tx :: Type' loc v
tx@(Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x)) ty :: Type' loc v
ty@(Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y)) = case (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y) of
  (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
_, VarT Origin loc
_ Name v
_) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi Type' loc v
tx Type' loc v
ty
  (ConT Origin loc
locA Name v
n [Fix (TypeF (Origin loc) (Name v))]
xs, ConT Origin loc
locB Name v
m [Fix (TypeF (Origin loc) (Name v))]
ys) ->
    if Name v
n Name v -> Name v -> Bool
forall a. Eq a => a -> a -> Bool
== Name v
m
      then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
      else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB
  (ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a1 Fix (TypeF (Origin loc) (Name v))
a2, ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b1 Fix (TypeF (Origin loc) (Name v))
b2) -> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
a1, Fix (TypeF (Origin loc) (Name v))
a2]) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
b1, Fix (TypeF (Origin loc) (Name v))
b2])
  (TupleT Origin loc
locA [Fix (TypeF (Origin loc) (Name v))]
as, TupleT Origin loc
locB [Fix (TypeF (Origin loc) (Name v))]
bs) ->
    if [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
bs
      then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
as) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
bs)
      else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB
  (ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a, ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
a) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
b)
  (VarT Origin loc
locA Name v
_, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
_) -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
ty)
  (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v))),
 TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v))))
_ -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
tx) (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
ty)
  where
    subtypeErr :: Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB = TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
      (TypeError loc (Name v)
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ loc
-> Type loc (Name v) -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr (Origin loc -> Origin loc -> loc
forall a. Show a => Origin a -> Origin a -> a
chooseUserOrigin Origin loc
locA Origin loc
locB) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
tx) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
ty)

subtypeOfL :: (IsVar v, Show loc)
  => Subst' loc v
  -> [Type' loc v]
  -> [Type' loc v]
  -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL :: Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
 -> Either (TypeError loc (Name v)) (Subst' loc v)
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
(Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)]
 -> Either (TypeError loc (Name v)) (Subst' loc v))
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ [Type' loc v] -> [Type' loc v] -> [(Type' loc v, Type' loc v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type' loc v]
as [Type' loc v]
bs
  where
    go :: (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) Either (TypeError loc (Name v)) (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either (TypeError loc (Name v)) (Subst' loc v)
eSubst

addDecls :: IsVar v
  => [Bind (Origin loc) (Name v) (Type' loc v)]
  -> Context' loc v
  -> InferM loc v (Context' loc v)
addDecls :: [Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls [Bind (Origin loc) (Name v) (Type' loc v)]
vs Context' loc v
ctx =
  (Context' loc v
 -> Bind (Origin loc) (Name v) (Type' loc v)
 -> InferM loc v (Context' loc v))
-> Context' loc v
-> [Bind (Origin loc) (Name v) (Type' loc v)]
-> InferM loc v (Context' loc v)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM  (\Context' loc v
c Bind (Origin loc) (Name v) (Type' loc v)
b -> VarSet' loc v
-> Bind (Origin loc) (Name v) (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
forall loc v.
IsVar v =>
VarSet' loc v
-> Bind' loc v (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecl VarSet' loc v
unknowns Bind (Origin loc) (Name v) (Type' loc v)
b Context' loc v
c) Context' loc v
ctx [Bind (Origin loc) (Name v) (Type' loc v)]
vs
  where
    unknowns :: VarSet' loc v
unknowns = (Signature (Origin loc) (Name v) -> VarSet' loc v)
-> Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Signature (Origin loc) (Name v) -> VarSet' loc v
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars (Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v)
-> Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v
forall a b. (a -> b) -> a -> b
$ Context' loc v -> Map (Name v) (Signature (Origin loc) (Name v))
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds Context' loc v
ctx

addDecl :: forall loc v . IsVar v
  => VarSet' loc v
  -> Bind' loc v (Type' loc v)
  -> Context' loc v
  -> InferM loc v (Context' loc v)
addDecl :: VarSet' loc v
-> Bind' loc v (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecl VarSet' loc v
unknowns Bind' loc v (Type' loc v)
b Context' loc v
ctx = do
  Signature' loc v
scheme <- VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
toScheme VarSet' loc v
unknowns (Bind' loc v (Type' loc v) -> Type' loc v
forall loc var a. Bind loc var a -> a
bind'rhs Bind' loc v (Type' loc v)
b)
  Context' loc v -> InferM loc v (Context' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Context' loc v -> InferM loc v (Context' loc v))
-> Context' loc v -> InferM loc v (Context' loc v)
forall a b. (a -> b) -> a -> b
$ Context' loc v
ctx
    { context'binds :: Map (Name v) (Signature' loc v)
context'binds = Name v
-> Signature' loc v
-> Map (Name v) (Signature' loc v)
-> Map (Name v) (Signature' loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Bind' loc v (Type' loc v) -> Name v
forall loc var a. Bind loc var a -> var
bind'lhs Bind' loc v (Type' loc v)
b) Signature' loc v
scheme (Map (Name v) (Signature' loc v)
 -> Map (Name v) (Signature' loc v))
-> (Context' loc v -> Map (Name v) (Signature' loc v))
-> Context' loc v
-> Map (Name v) (Signature' loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' loc v -> Map (Name v) (Signature' loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds (Context' loc v -> Map (Name v) (Signature' loc v))
-> Context' loc v -> Map (Name v) (Signature' loc v)
forall a b. (a -> b) -> a -> b
$ Context' loc v
ctx }
  where
    toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
    toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
toScheme VarSet' loc v
uVars Type' loc v
ty = do
      (Subst (Origin loc) (Name v)
subst, [(Origin loc, Name v)]
newVars) <- ([((Origin loc, Name v), Name v)]
 -> (Subst (Origin loc) (Name v), [(Origin loc, Name v)]))
-> InferM loc v [((Origin loc, Name v), Name v)]
-> InferM
     loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[((Origin loc, Name v), Name v)]
xs -> ([((Origin loc, Name v), Name v)] -> Subst (Origin loc) (Name v)
forall loc. [((loc, Name v), Name v)] -> Subst loc (Name v)
toSubst [((Origin loc, Name v), Name v)]
xs, (((Origin loc, Name v), Name v) -> (Origin loc, Name v))
-> [((Origin loc, Name v), Name v)] -> [(Origin loc, Name v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((Origin loc
loc, Name v
_), Name v
v) -> (Origin loc
loc, Name v
v)) [((Origin loc, Name v), Name v)]
xs)) (InferM loc v [((Origin loc, Name v), Name v)]
 -> InferM
      loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)]))
-> InferM loc v [((Origin loc, Name v), Name v)]
-> InferM
     loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)])
forall a b. (a -> b) -> a -> b
$
          ((Origin loc, Name v)
 -> InferM loc v ((Origin loc, Name v), Name v))
-> [(Origin loc, Name v)]
-> InferM loc v [((Origin loc, Name v), Name v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Origin loc, Name v)
sv -> (Name v -> ((Origin loc, Name v), Name v))
-> InferM loc v (Name v)
-> InferM loc v ((Origin loc, Name v), Name v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Origin loc, Name v)
sv, )) InferM loc v (Name v)
forall v loc. IsVar v => InferM loc v (Name v)
freshVar) ([(Origin loc, Name v)]
 -> InferM loc v [((Origin loc, Name v), Name v)])
-> [(Origin loc, Name v)]
-> InferM loc v [((Origin loc, Name v), Name v)]
forall a b. (a -> b) -> a -> b
$ VarSet' loc v -> [(Origin loc, Name v)]
forall src var. VarSet src var -> [(src, var)]
varSetToList VarSet' loc v
schematicVars
      Signature' loc v -> InferM loc v (Signature' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signature' loc v -> InferM loc v (Signature' loc v))
-> Signature' loc v -> InferM loc v (Signature' loc v)
forall a b. (a -> b) -> a -> b
$ ((Origin loc, Name v) -> Signature' loc v -> Signature' loc v)
-> Signature' loc v -> [(Origin loc, Name v)] -> Signature' loc v
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Origin loc -> Name v -> Signature' loc v -> Signature' loc v)
-> (Origin loc, Name v) -> Signature' loc v -> Signature' loc v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Origin loc -> Name v -> Signature' loc v -> Signature' loc v
forall loc v. loc -> v -> Signature loc v -> Signature loc v
forAllT) (Type' loc v -> Signature' loc v
forall loc src. Type loc src -> Signature loc src
monoT (Subst (Origin loc) (Name v) -> Type' loc v -> Type' loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
subst Type' loc v
ty)) [(Origin loc, Name v)]
newVars
      where
        schematicVars :: VarSet' loc v
schematicVars = Type' loc v -> VarSet' loc v
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type' loc v
ty VarSet' loc v -> VarSet' loc v -> VarSet' loc v
forall var src.
Ord var =>
VarSet src var -> VarSet src var -> VarSet src var
`differenceVarSet` VarSet' loc v
uVars

    toSubst :: [((loc, Name v), Name v)] -> Subst loc (Name v)
toSubst = Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v))
-> ([((loc, Name v), Name v)] -> Map (Name v) (Type loc (Name v)))
-> [((loc, Name v), Name v)]
-> Subst loc (Name v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name v, Type loc (Name v))] -> Map (Name v) (Type loc (Name v))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name v, Type loc (Name v))] -> Map (Name v) (Type loc (Name v)))
-> ([((loc, Name v), Name v)] -> [(Name v, Type loc (Name v))])
-> [((loc, Name v), Name v)]
-> Map (Name v) (Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((loc, Name v), Name v) -> (Name v, Type loc (Name v)))
-> [((loc, Name v), Name v)] -> [(Name v, Type loc (Name v))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((loc
loc, Name v
v), Name v
a) -> (Name v
v, loc -> Name v -> Type loc (Name v)
forall loc var. loc -> var -> Type loc var
varT loc
loc Name v
a))

-------------------------------------------------------
-- pretty letters for variables in the result type

-- | Converts variable names to human-readable format.
normaliseType :: (HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) => m loc (Name v) -> m loc (Name v)
normaliseType :: m loc (Name v) -> m loc (Name v)
normaliseType m loc (Name v)
ty = Subst loc (Name v) -> m loc (Name v) -> m loc (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply (m loc (Name v) -> Subst loc (Name v)
forall (m :: * -> * -> *) loc v.
(HasTypeVars m, Show loc, Eq loc, IsVar v) =>
m loc v -> Subst loc v
normaliseSubst m loc (Name v)
ty) m loc (Name v)
ty

normaliseSubst :: (HasTypeVars m, Show loc, Eq loc, IsVar v) => m loc v -> Subst loc v
normaliseSubst :: m loc v -> Subst loc v
normaliseSubst m loc v
x =
  Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> Map v (Type loc v) -> Subst loc v
forall a b. (a -> b) -> a -> b
$ [(v, Type loc v)] -> Map v (Type loc v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(v, Type loc v)] -> Map v (Type loc v))
-> [(v, Type loc v)] -> Map v (Type loc v)
forall a b. (a -> b) -> a -> b
$
    ((v, loc) -> v -> (v, Type loc v))
-> [(v, loc)] -> [v] -> [(v, Type loc v)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(v
nameA, loc
loc) v
nameB -> (v
nameA, loc -> v -> Type loc v
forall loc var. loc -> var -> Type loc var
varT loc
loc v
nameB)) (m loc v -> [(v, loc)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder m loc v
x) [v]
forall v. IsVar v => [v]
prettyLetters

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

-- | Checks weather two types unify. If they do it returns substitution that unifies them.
unifyTypes :: (Show loc, IsVar v, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
unifyTypes :: Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
unifyTypes Type loc v
a Type loc v
b =
  Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
 -> Either (TypeError loc v) (Subst loc v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ (TypeError loc (Name v) -> TypeError loc v)
-> (Subst (Origin loc) (Name v)
    -> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeError loc (Name v) -> TypeError loc v
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError loc (Name v) -> TypeError loc v)
-> (TypeError loc (Name v) -> TypeError loc (Name v))
-> TypeError loc (Name v)
-> TypeError loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError loc (Name v) -> TypeError loc (Name v)
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
forall v loc.
Ord v =>
Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v))
-> (Subst (Origin loc) (Name v) -> Subst loc (Name v))
-> Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) (Name v) -> Subst loc (Name v)
forall v loc. Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
 -> Either
      (TypeError loc v) (Either (TypeError loc v) (Subst loc v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
     (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall a b. (a -> b) -> a -> b
$
    Subst (Origin loc) (Name v)
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin loc) (Name v)
forall a. Monoid a => a
mempty ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
Proven Type loc v
a) ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode Type loc v
b)

------------------------------------------------
-- recover name and origin wrappers

fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar = (TypeError loc var -> TypeError loc var)
-> (TypeError loc var -> TypeError loc var)
-> Either (TypeError loc var) (TypeError loc var)
-> TypeError loc var
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TypeError loc var -> TypeError loc var
forall a. a -> a
id TypeError loc var -> TypeError loc var
forall a. a -> a
id (Either (TypeError loc var) (TypeError loc var)
 -> TypeError loc var)
-> (TypeError loc (Name var)
    -> Either (TypeError loc var) (TypeError loc var))
-> TypeError loc (Name var)
-> TypeError loc var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    OccursErr loc
loc Type loc (Name var)
ty     -> (Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc -> Type loc var -> TypeError loc var
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
ty)
    UnifyErr loc
loc Type loc (Name var)
tA Type loc (Name var)
tB   -> (Type loc var -> Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (loc -> Type loc var -> Type loc var -> TypeError loc var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tA) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tB)
    SubtypeErr loc
loc Type loc (Name var)
tA Type loc (Name var)
tB -> (Type loc var -> Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (loc -> Type loc var -> Type loc var -> TypeError loc var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tA) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tB)
    NotInScopeErr loc
loc Name var
v  -> (var -> TypeError loc var)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc -> var -> TypeError loc var
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr loc
loc) (Either (TypeError loc var) var
 -> Either (TypeError loc var) (TypeError loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
    EmptyCaseExpr loc
loc    -> TypeError loc var -> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError loc var
 -> Either (TypeError loc var) (TypeError loc var))
-> TypeError loc var
-> Either (TypeError loc var) (TypeError loc var)
forall a b. (a -> b) -> a -> b
$ loc -> TypeError loc var
forall loc var. loc -> TypeError loc var
EmptyCaseExpr loc
loc
    ConsArityMismatch loc
loc Name var
v Int
expected Int
actual -> (var -> TypeError loc var)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
x -> loc -> var -> Int -> Int -> TypeError loc var
forall loc var. loc -> var -> Int -> Int -> TypeError loc var
ConsArityMismatch loc
loc var
x Int
expected Int
actual) (Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v)
    TypeError loc (Name var)
FreshNameFound       -> TypeError loc var -> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeError loc var
forall loc var. TypeError loc var
FreshNameFound

fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar (Type Fix (TypeF loc (Name var))
x) = (Fix (TypeF loc var) -> Type loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Type loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Either (TypeError loc var) (Fix (TypeF loc var))
 -> Either (TypeError loc var) (Type loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Type loc var)
forall a b. (a -> b) -> a -> b
$ (TypeF loc (Name var) (Fix (TypeF loc var))
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc (Name var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall loc var.
TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
go Fix (TypeF loc (Name var))
x
  where
    go :: TypeF loc (Name var) (Fix (TypeF loc var)) -> Either (TypeError loc var) (Fix (TypeF loc var))
    go :: TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
go = \case
      VarT loc
loc Name var
v     -> (var -> Fix (TypeF loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> (var -> TypeF loc var (Fix (TypeF loc var)))
-> var
-> Fix (TypeF loc var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. loc -> var -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> var -> TypeF loc var r
VarT loc
loc) (Either (TypeError loc var) var
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
      ConT loc
loc Name var
v [Fix (TypeF loc var)]
as  -> (var -> Fix (TypeF loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
con -> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc
-> var
-> [Fix (TypeF loc var)]
-> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> var -> [r] -> TypeF loc var r
ConT loc
loc var
con [Fix (TypeF loc var)]
as) (Either (TypeError loc var) var
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
      ArrowT loc
loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (TypeF loc var)
-> Fix (TypeF loc var)
-> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> r -> r -> TypeF loc var r
ArrowT loc
loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b
      TupleT loc
loc [Fix (TypeF loc var)]
as  -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc -> [Fix (TypeF loc var)] -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> [r] -> TypeF loc var r
TupleT loc
loc [Fix (TypeF loc var)]
as
      ListT loc
loc Fix (TypeF loc var)
as   -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
 -> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc -> Fix (TypeF loc var) -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> r -> TypeF loc var r
ListT loc
loc Fix (TypeF loc var)
as

fromTyTermNameVar :: TyTerm prim loc (Name var) -> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar :: TyTerm prim loc (Name var)
-> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar (TyTerm Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
x) = (Fix (Ann (Type loc var) (TermF prim loc var))
 -> TyTerm prim loc var)
-> Either
     (TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either (TypeError loc var) (TyTerm prim loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (Ann (Type loc var) (TermF prim loc var))
-> TyTerm prim loc var
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm (Either
   (TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> Either (TypeError loc var) (TyTerm prim loc var))
-> Either
     (TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either (TypeError loc var) (TyTerm prim loc var)
forall a b. (a -> b) -> a -> b
$ (Ann
   (Type loc (Name var))
   (TermF prim loc (Name var))
   (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> Either
      (TypeError loc var)
      (Fix (Ann (Type loc var) (TermF prim loc var))))
-> Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
-> Either
     (TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM Ann
  (Type loc (Name var))
  (TermF prim loc (Name var))
  (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either
     (TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
forall t v prim.
Ann
  (Type t (Name v))
  (TermF prim t (Name v))
  (Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
go Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
x
  where
    go :: Ann
  (Type t (Name v))
  (TermF prim t (Name v))
  (Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
go (Ann Type t (Name v)
annTy TermF prim t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
term) = (Type t v
 -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
 -> Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Type t v)
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\Type t v
t TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
val -> Ann
  (Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
   (Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
 -> Fix (Ann (Type t v) (TermF prim t v)))
-> Ann
     (Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
forall a b. (a -> b) -> a -> b
$ Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Ann
     (Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann Type t v
t TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
val) (Type t (Name v) -> Either (TypeError t v) (Type t v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type t (Name v)
annTy) (Either
   (TypeError t v)
   (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
 -> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall a b. (a -> b) -> a -> b
$ case TermF prim t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
term of
      Var t
loc Name v
v           -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Var t
loc) (Either (TypeError t v) v
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) v
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
      Prim t
loc prim
p          -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t -> prim -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> prim -> TermF prim loc v r
Prim t
loc prim
p
      App t
loc Fix (Ann (Type t v) (TermF prim t v))
a Fix (Ann (Type t v) (TermF prim t v))
b         -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t
-> Fix (Ann (Type t v) (TermF prim t v))
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> r -> r -> TermF prim loc v r
App t
loc Fix (Ann (Type t v) (TermF prim t v))
a Fix (Ann (Type t v) (TermF prim t v))
b
      Lam t
loc Name v
v Fix (Ann (Type t v) (TermF prim t v))
a         -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\v
arg -> t
-> v
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> r -> TermF prim loc v r
Lam t
loc v
arg Fix (Ann (Type t v) (TermF prim t v))
a) (Either (TypeError t v) v
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) v
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
      Let t
loc Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
bind Fix (Ann (Type t v) (TermF prim t v))
a      -> (Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
 -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
b -> t
-> Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> Bind loc v r -> r -> TermF prim loc v r
Let t
loc Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
b Fix (Ann (Type t v) (TermF prim t v))
a) (Either
   (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
     (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
forall loc var a loc.
Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
bind
      LetRec t
loc [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
binds Fix (Ann (Type t v) (TermF prim t v))
a  -> ([Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
 -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
bs -> t
-> [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r.
loc -> [Bind loc v r] -> r -> TermF prim loc v r
LetRec t
loc [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
bs Fix (Ann (Type t v) (TermF prim t v))
a) (Either
   (TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
     (TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ (Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
 -> Either
      (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
forall loc var a loc.
Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
binds
      AssertType t
loc Fix (Ann (Type t v) (TermF prim t v))
a Type t (Name v)
ty -> (Type t v
 -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Type t v)
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
-> Fix (Ann (Type t v) (TermF prim t v))
-> Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> r -> Type loc v -> TermF prim loc v r
AssertType t
loc Fix (Ann (Type t v) (TermF prim t v))
a) (Either (TypeError t v) (Type t v)
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) (Type t v)
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Type t (Name v) -> Either (TypeError t v) (Type t v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type t (Name v)
ty
      Constr t
loc Name v
v        -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Constr t
loc) (Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v)
      Bottom t
loc          -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> TermF prim loc v r
Bottom t
loc
      Case t
loc Fix (Ann (Type t v) (TermF prim t v))
e [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
alts     -> ([CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
 -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
     (TypeError t v)
     [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
-> Fix (Ann (Type t v) (TermF prim t v))
-> [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case t
loc Fix (Ann (Type t v) (TermF prim t v))
e) (Either
   (TypeError t v)
   [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
 -> Either
      (TypeError t v)
      (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
     (TypeError t v)
     [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v)
     (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ (CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
 -> Either
      (TypeError t v)
      (CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
     (TypeError t v)
     [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
     (TypeError t v)
     (CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v))))
forall t t a loc.
CaseAlt t (Name t) a -> Either (TypeError loc t) (CaseAlt t t a)
fromAlt [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
alts

    fromBind :: Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind Bind loc (Name var) a
b = (var -> Bind loc var a)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
a -> Bind loc (Name var) a
b { bind'lhs :: var
bind'lhs = var
a }) (Either (TypeError loc var) var
 -> Either (TypeError loc var) (Bind loc var a))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var a)
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar (Name var -> Either (TypeError loc var) var)
-> Name var -> Either (TypeError loc var) var
forall a b. (a -> b) -> a -> b
$ Bind loc (Name var) a -> Name var
forall loc var a. Bind loc var a -> var
bind'lhs Bind loc (Name var) a
b

    fromAlt :: CaseAlt t (Name t) a -> Either (TypeError loc t) (CaseAlt t t a)
fromAlt alt :: CaseAlt t (Name t) a
alt@CaseAlt{a
t
[(t, Name t)]
Name t
caseAlt'rhs :: a
caseAlt'args :: [(t, Name t)]
caseAlt'tag :: Name t
caseAlt'loc :: t
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
..} =
      (t -> [(t, t)] -> CaseAlt t t a)
-> Either (TypeError loc t) t
-> Either (TypeError loc t) [(t, t)]
-> Either (TypeError loc t) (CaseAlt t t a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\t
tag [(t, t)]
args -> CaseAlt t (Name t) a
alt { caseAlt'tag :: t
caseAlt'tag = t
tag, caseAlt'args :: [(t, t)]
caseAlt'args = [(t, t)]
args })
        (Name t -> Either (TypeError loc t) t
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name t
caseAlt'tag)
        (((t, Name t) -> Either (TypeError loc t) (t, t))
-> [(t, Name t)] -> Either (TypeError loc t) [(t, t)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (t, Name t) -> Either (TypeError loc t) (t, t)
forall t t loc. (t, Name t) -> Either (TypeError loc t) (t, t)
fromAltArg [(t, Name t)]
caseAlt'args)

    fromAltArg :: (t, Name t) -> Either (TypeError loc t) (t, t)
fromAltArg (t
loc, Name t
v) = (t -> (t, t))
-> Either (TypeError loc t) t -> Either (TypeError loc t) (t, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
loc , ) (Name t -> Either (TypeError loc t) t
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name t
v)

fromSubstNameVar :: Ord v => Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar :: Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst Map (Name v) (Type loc (Name v))
m) = ([(v, Type loc v)] -> Subst loc v)
-> Either (TypeError loc v) [(v, Type loc v)]
-> Either (TypeError loc v) (Subst loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> ([(v, Type loc v)] -> Map v (Type loc v))
-> [(v, Type loc v)]
-> Subst loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(v, Type loc v)] -> Map v (Type loc v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList) (Either (TypeError loc v) [(v, Type loc v)]
 -> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) [(v, Type loc v)]
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ ((Name v, Type loc (Name v))
 -> Either (TypeError loc v) (v, Type loc v))
-> [(Name v, Type loc (Name v))]
-> Either (TypeError loc v) [(v, Type loc v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name v, Type loc (Name v))
-> Either (TypeError loc v) (v, Type loc v)
forall a loc.
(Name a, Type loc (Name a))
-> Either (TypeError loc a) (a, Type loc a)
uncover ([(Name v, Type loc (Name v))]
 -> Either (TypeError loc v) [(v, Type loc v)])
-> [(Name v, Type loc (Name v))]
-> Either (TypeError loc v) [(v, Type loc v)]
forall a b. (a -> b) -> a -> b
$ Map (Name v) (Type loc (Name v)) -> [(Name v, Type loc (Name v))]
forall k a. Map k a -> [(k, a)]
M.toList Map (Name v) (Type loc (Name v))
m
  where
    uncover :: (Name a, Type loc (Name a))
-> Either (TypeError loc a) (a, Type loc a)
uncover (Name a
v, Type loc (Name a)
ty) = (a -> Type loc a -> (a, Type loc a))
-> Either (TypeError loc a) a
-> Either (TypeError loc a) (Type loc a)
-> Either (TypeError loc a) (a, Type loc a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (Name a -> Either (TypeError loc a) a
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name a
v) (Type loc (Name a) -> Either (TypeError loc a) (Type loc a)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name a)
ty)

fromSubstOrigin :: Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin :: Subst (Origin loc) v -> Subst loc v
fromSubstOrigin = Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> (Subst (Origin loc) v -> Map v (Type loc v))
-> Subst (Origin loc) v
-> Subst loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type (Origin loc) v -> Type loc v)
-> Map v (Type (Origin loc) v) -> Map v (Type loc v)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Origin loc -> loc) -> Type (Origin loc) v -> Type loc v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin) (Map v (Type (Origin loc) v) -> Map v (Type loc v))
-> (Subst (Origin loc) v -> Map v (Type (Origin loc) v))
-> Subst (Origin loc) v
-> Map v (Type loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) v -> Map v (Type (Origin loc) v)
forall loc v. Subst loc v -> Map v (Type loc v)
unSubst

-- | Substitutes all type arguments with given types.
closeSignature :: Ord var => [Type loc var] -> Signature loc var -> Type loc var
closeSignature :: [Type loc var] -> Signature loc var -> Type loc var
closeSignature [Type loc var]
argTys Signature loc var
sig = Subst loc var -> Type loc var -> Type loc var
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply (Map var (Type loc var) -> Subst loc var
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map var (Type loc var) -> Subst loc var)
-> Map var (Type loc var) -> Subst loc var
forall a b. (a -> b) -> a -> b
$ [(var, Type loc var)] -> Map var (Type loc var)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(var, Type loc var)] -> Map var (Type loc var))
-> [(var, Type loc var)] -> Map var (Type loc var)
forall a b. (a -> b) -> a -> b
$ [var] -> [Type loc var] -> [(var, Type loc var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [var]
argNames [Type loc var]
argTys) Type loc var
monoTy
  where
    ([var]
argNames, Type loc var
monoTy) = Signature loc var -> ([var], Type loc var)
forall loc var. Signature loc var -> ([var], Type loc var)
splitSignature Signature loc var
sig

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

-- | Pretty printer for result of type-inference
printInfer :: (PrettyLang q) => (Either [ErrorOf q] (TypeOf q)) -> IO ()
printInfer :: Either [ErrorOf q] (TypeOf q) -> IO ()
printInfer = \case
  Right TypeOf q
ty  -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ TypeOf q -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty TypeOf q
ty
  Left [ErrorOf q]
errs -> (ErrorOf q -> IO ()) -> [ErrorOf q] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> (ErrorOf q -> String) -> ErrorOf q -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") ShowS -> (ErrorOf q -> String) -> ErrorOf q -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (ErrorOf q -> Doc Any) -> ErrorOf q -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorOf q -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty) [ErrorOf q]
errs