-- | 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
  , ContextOf
  -- * Inference
  , inferType
  , inferTerm
  , subtypeOf
  , unifyTypes
  -- * Utils
  , closeSignature
) where

import Control.Monad.Identity

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 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.
newtype Context loc v = Context { Context loc v -> Map v (Signature loc v)
unContext :: Map v (Signature loc v) }
  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, b -> Context loc v -> Context loc v
NonEmpty (Context loc v) -> Context loc v
Context loc v -> Context loc v -> Context loc v
(Context loc v -> Context loc v -> Context loc v)
-> (NonEmpty (Context loc v) -> Context loc v)
-> (forall b. Integral b => b -> Context loc v -> Context loc v)
-> Semigroup (Context loc v)
forall b. Integral b => b -> Context loc v -> Context loc v
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall loc v. Ord v => NonEmpty (Context loc v) -> Context loc v
forall loc v.
Ord v =>
Context loc v -> Context loc v -> Context loc v
forall loc v b.
(Ord v, Integral b) =>
b -> Context loc v -> Context loc v
stimes :: b -> Context loc v -> Context loc v
$cstimes :: forall loc v b.
(Ord v, Integral b) =>
b -> Context loc v -> Context loc v
sconcat :: NonEmpty (Context loc v) -> Context loc v
$csconcat :: forall loc v. Ord v => NonEmpty (Context loc v) -> Context loc v
<> :: Context loc v -> Context loc v -> Context loc v
$c<> :: forall loc v.
Ord v =>
Context loc v -> Context loc v -> Context loc v
Semigroup, Semigroup (Context loc v)
Context loc v
Semigroup (Context loc v)
-> Context loc v
-> (Context loc v -> Context loc v -> Context loc v)
-> ([Context loc v] -> Context loc v)
-> Monoid (Context loc v)
[Context loc v] -> Context loc v
Context loc v -> Context loc v -> Context loc v
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall loc v. Ord v => Semigroup (Context loc v)
forall loc v. Ord v => Context loc v
forall loc v. Ord v => [Context loc v] -> Context loc v
forall loc v.
Ord v =>
Context loc v -> Context loc v -> Context loc v
mconcat :: [Context loc v] -> Context loc v
$cmconcat :: forall loc v. Ord v => [Context loc v] -> Context loc v
mappend :: Context loc v -> Context loc v -> Context loc v
$cmappend :: forall loc v.
Ord v =>
Context loc v -> Context loc v -> Context loc v
mempty :: Context loc v
$cmempty :: forall loc v. Ord v => Context loc v
$cp1Monoid :: forall loc v. Ord v => Semigroup (Context loc v)
Monoid)

-- | 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 = Map v (Signature loc v) -> Context loc v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Context loc v)
-> (Context loc v -> Map v (Signature loc v))
-> Context loc v
-> Context loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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))
-> (Context loc v -> Map v (Signature loc v))
-> Context loc v
-> Map v (Signature loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context loc v -> Map v (Signature loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
unContext

-- | 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)
ctx) = Map v (Signature loc v) -> Context loc v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Context loc v)
-> Map v (Signature loc v) -> Context loc v
forall a b. (a -> b) -> a -> b
$ 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)
ctx

-- | 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)
ctx) = 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)
ctx

-- | 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)
ctx) = Map v (Signature loc v) -> Context loc v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Context loc v)
-> Map v (Signature loc v) -> Context loc v
forall a b. (a -> b) -> a -> b
$ 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)
ctx Map v ()
fv
  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 lprim oc. Ord v => Term lprim oc 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)
m) = Map v (Signature loc v) -> Context loc v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Context loc v)
-> Map v (Signature loc v) -> Context loc v
forall a b. (a -> b) -> a -> b
$ (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 v) -> Map v (Signature loc v)
forall a b. (a -> b) -> a -> b
$ (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) Map k1 (Signature loc k1)
m

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 = Map v (Signature (Origin loc) v) -> Context (Origin loc) v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map v (Signature (Origin loc) v) -> Context (Origin loc) v)
-> (Context loc v -> Map v (Signature (Origin loc) v))
-> Context loc v
-> Context (Origin loc) v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signature loc v -> Signature (Origin loc) v)
-> Map v (Signature loc v) -> Map v (Signature (Origin loc) v)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((loc -> Origin loc) -> Signature loc v -> Signature (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) (Map v (Signature loc v) -> Map v (Signature (Origin loc) v))
-> (Context loc v -> Map v (Signature loc v))
-> Context loc v
-> Map v (Signature (Origin loc) v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context loc v -> Map v (Signature loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
unContext

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 (Except (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, MonadError (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 (Except (TypeError loc (Name var))) a
m) = Except (TypeError loc (Name var)) a
-> Either (TypeError loc (Name var)) a
forall e a. Except e a -> Either e a
runExcept (Except (TypeError loc (Name var)) a
 -> Either (TypeError loc (Name var)) a)
-> Except (TypeError loc (Name var)) a
-> Either (TypeError loc (Name var)) a
forall a b. (a -> b) -> a -> b
$ StateT Int (Except (TypeError loc (Name var))) a
-> Int -> Except (TypeError loc (Name var)) a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT Int (Except (TypeError loc (Name var))) a
m Int
0

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 = Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q))
-> Either (ErrorOf q) (TyTermOf q)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q))
 -> Either (ErrorOf q) (TyTermOf q))
-> Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q))
-> Either (ErrorOf q) (TyTermOf q)
forall a b. (a -> b) -> a -> b
$
  (TypeError (Src q) (Name (Var q)) -> ErrorOf q)
-> ((Subst (Origin (Src q)) (Name (Var q)),
     TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
    -> Either (ErrorOf q) (TyTermOf q))
-> Either
     (TypeError (Src q) (Name (Var q)))
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (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) ((\(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)) (Either
   (TypeError (Src q) (Name (Var q)))
   (Subst (Origin (Src q)) (Name (Var q)),
    TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
 -> Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q)))
-> Either
     (TypeError (Src q) (Name (Var q)))
     (Subst (Origin (Src q)) (Name (Var q)),
      TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either (ErrorOf q) (Either (ErrorOf q) (TyTermOf q))
forall a b. (a -> b) -> a -> b
$
    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)
  where
    toTyTerm :: TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
toTyTerm = 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)
                        )

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 Type (Origin (Src q)) (Name (Var q))
ty Name (Var q)
tag   -> Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Name (Var q)
-> InferOf q
forall q.
Lang q =>
Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q
inferConstr Origin (Src q)
loc Type (Origin (Src q)) (Name (Var q))
ty 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

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)
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name (Var q)
v (ContextOf' q
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall loc v. Context loc v -> Map v (Signature loc v)
unContext ContextOf' q
ctx) of
    Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing  -> TypeError (Src q) (Name (Var q)) -> InferOf q
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError (Src q) (Name (Var q)) -> InferOf q)
-> TypeError (Src q) (Name (Var q)) -> InferOf q
forall a b. (a -> b) -> a -> b
$ 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
    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
$ Prim q -> Type (Src q) (Var q)
forall q. Lang q => Prim q -> TypeOf q
getPrimType 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')]) -> (Subst' (Src q) (Var q)
 -> (Subst' (Src q) (Var q),
     TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM (Src q) (Var q) (Subst' (Src q) (Var q)) -> InferOf q
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\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)
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
term)) (InferM (Src q) (Var q) (Subst' (Src q) (Var q)) -> InferOf q)
-> InferM (Src q) (Var q) (Subst' (Src q) (Var q)) -> InferOf q
forall a b. (a -> b) -> a -> b
$ Subst' (Src q) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Subst' (Src q) (Var q))
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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)
    (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 r. Bind loc var r -> r
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)))
-> ContextOf' q
forall 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)) [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
  (ContextOf' q
ctx1, [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx1, Subst (Origin (Src q)) (Name (Var q))
subst) <- ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> [Type' (Src q) (Var q)]
-> InferM
     (Src q)
     (Var q)
     (ContextOf' q,
      [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))],
      Subst (Origin (Src q)) (Name (Var q)))
forall v (f :: * -> * -> *) (f :: * -> *) loc a.
(CanApply f, IsVar v, MonadError (TypeError loc (Name v)) f,
 Show loc) =>
f (Origin loc) (Name v)
-> [(a, Signature (Origin loc) (Name v))]
-> Subst (Origin loc) (Name v)
-> [Type' loc v]
-> f (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
  [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
  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 r. Bind loc var r -> r
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 r. Bind loc var r -> 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 r. Bind loc var r -> 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 r. Bind loc var r -> 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]
-> f (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)))
-> f (Subst (Origin loc) (Name v))
-> f (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)) (f (Subst (Origin loc) (Name v))
 -> f (f (Origin loc) (Name v),
       [(a, Signature (Origin loc) (Name v))],
       Subst (Origin loc) (Name v)))
-> f (Subst (Origin loc) (Name v))
-> f (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]
-> f (Subst (Origin loc) (Name v))
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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 r. loc -> var -> r -> Bind loc var r
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
  Subst' (Src q) (Var q)
subst <- Subst' (Src q) (Var q)
-> TypeOf' q
-> TypeOf' q
-> InferM (Src q) (Var q) (Subst' (Src q) (Var q))
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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)
  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)

inferConstr :: Lang q => Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q
inferConstr :: Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q
inferConstr Origin (Src q)
loc TypeOf' q
ty Name (Var q)
tag = do
  TypeOf' q
vT <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (TypeOf' 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) (TypeOf' q))
-> Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (TypeOf' q)
forall a b. (a -> b) -> a -> b
$ TypeOf' q -> Signature (Origin (Src q)) (Name (Var q))
forall loc v. (Eq loc, Ord v) => Type loc v -> Signature loc v
typeToSignature TypeOf' 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)
-> TypeOf' 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 TypeOf' q
vT Name (Var q)
tag)

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
  (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))
-> Type (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)),
      [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)
      (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)
     (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
  (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)))]
 -> 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 a b. (a -> b) -> a -> b
$ (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)))]
-> [CaseAlt
      (Origin (Src q))
      (Name (Var q))
      (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 v (f :: * -> * -> *) loc.
(Ord v, CanApply f) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
psi) [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyAlts)
  where
    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (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)
     (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 =
      ((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)))])
 -> (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)
     (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)
     (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 b. Functor f => (a -> b) -> f a -> f b
fmap (\(Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
_, Type (Origin (Src q)) (Name (Var q))
tRes, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
as) -> (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)) (InferM
   (Src q)
   (Var q)
   (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)
      (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)
     (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)
     (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
$ ((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)))])
 -> CaseAltOf' q (TermOf' q)
 -> InferM
      (Src q)
      (Var q)
      (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)))]))
-> (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)))])
-> [CaseAltOf' q (TermOf' q)]
-> InferM
     (Src q)
     (Var q)
     (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 (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)),
 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)),
      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, Type (Origin (Src q)) (Name (Var q))
tE, []) [CaseAltOf' q (TermOf' q)]
alts
      where
        go :: (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)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (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)))])
go (Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
tyTop, Type (Origin (Src q)) (Name (Var q))
_, [CaseAlt
   (Origin (Src q))
   (Name (Var q))
   (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res) CaseAltOf' q (TermOf' q)
alt = do
          (Subst (Origin (Src q)) (Name (Var q))
phi, Type (Origin (Src q)) (Name (Var q))
tRes, CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1) <- CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (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))))
inferAlt (Subst (Origin (Src q)) (Name (Var q))
-> CaseAltOf' q (TermOf' q) -> CaseAltOf' q (TermOf' q)
forall v (f :: * -> * -> *) loc.
(Ord v, CanApply f) =>
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)
          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
          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))
-> InferM (Src q) (Var q) (Subst (Origin (Src q)) (Name (Var q)))
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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))
 -> Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v a. CaseAlt loc v a -> Type loc v
caseAlt'constrType CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1)
          (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)
     (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 (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, 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))
tRes, 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 v (f :: * -> * -> *) loc.
(Ord v, CanApply f) =>
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)


    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q))
    inferAlt :: CaseAltOf' q (TermOf' q)
-> InferM
     (Src q)
     (Var q)
     (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))))
inferAlt CaseAltOf' q (TermOf' q)
preAlt = do
      CaseAltOf' q (TermOf' q)
alt <- CaseAltOf' q (TermOf' q)
-> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
newCaseAltInstance CaseAltOf' q (TermOf' q)
preAlt
      let argVars :: [(Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars = (Typed
   (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)))))
-> [Typed
      (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap  (\Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty -> ((Origin (Src q), Name (Var q)) -> Name (Var q)
forall a b. (a, b) -> b
snd ((Origin (Src q), Name (Var q)) -> Name (Var q))
-> (Origin (Src q), Name (Var q)) -> Name (Var q)
forall a b. (a -> b) -> a -> b
$ Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
-> (Origin (Src q), Name (Var q))
forall loc v a. Typed loc v a -> a
typed'value Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty, ((Origin (Src q), Name (Var q)) -> Origin (Src q)
forall a b. (a, b) -> a
fst ((Origin (Src q), Name (Var q)) -> Origin (Src q))
-> (Origin (Src q), Name (Var q)) -> Origin (Src q)
forall a b. (a -> b) -> a -> b
$ Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
-> (Origin (Src q), Name (Var q))
forall loc v a. Typed loc v a -> a
typed'value Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty, Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v a. Typed loc v a -> Type loc v
typed'type Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty))) ([Typed
    (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))))])
-> [Typed
      (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. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q)
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt
          ctx1 :: ContextOf' q
ctx1 = Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> ContextOf' q
forall 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) 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 args :: [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
args = ((Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
 -> Typed
      (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))))]
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Name (Var q)
v, (Origin (Src q)
argLoc, Type (Origin (Src q)) (Name (Var q))
tv)) -> Type (Origin (Src q)) (Name (Var q))
-> (Origin (Src q), Name (Var q))
-> Typed
     (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
forall loc v a. Type loc v -> a -> Typed loc v a
Typed (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))
subst Type (Origin (Src q)) (Name (Var q))
tv) (Origin (Src q)
argLoc, Name (Var q)
v)) [(Name (Var q),
  (Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars
          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
                  , caseAlt'args :: [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
caseAlt'args = [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
args
                  , caseAlt'constrType :: Type (Origin (Src q)) (Name (Var q))
caseAlt'constrType = 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))
subst (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 a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Type (Origin (Src q)) (Name (Var q))
forall loc v a. CaseAlt loc v a -> Type loc v
caseAlt'constrType CaseAltOf' q (TermOf' q)
alt
                  }
      (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)
     (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 (m :: * -> *) a. Monad m => a -> m a
return (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, CaseAlt
  (Origin (Src q))
  (Name (Var q))
  (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt')

    newCaseAltInstance :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
    newCaseAltInstance :: CaseAltOf' q (TermOf' q)
-> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
newCaseAltInstance CaseAltOf' q (TermOf' q)
alt = do
      Type (Origin (Src q)) (Name (Var q))
tv <- 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
$ Type (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall loc v. (Eq loc, Ord v) => Type loc v -> Signature loc v
typeToSignature (Type (Origin (Src q)) (Name (Var q))
 -> Signature (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Type (Origin (Src q)) (Name (Var q))
getCaseType CaseAltOf' q (TermOf' q)
alt
      let ([Type (Origin (Src q)) (Name (Var q))]
argsT, Type (Origin (Src q)) (Name (Var q))
resT)= 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))
tv
      CaseAltOf' q (TermOf' q)
-> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseAltOf' q (TermOf' q)
 -> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q)))
-> CaseAltOf' q (TermOf' q)
-> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q)
alt
        { caseAlt'constrType :: Type (Origin (Src q)) (Name (Var q))
caseAlt'constrType = Type (Origin (Src q)) (Name (Var q))
resT
        , caseAlt'args :: [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
caseAlt'args = (Type (Origin (Src q)) (Name (Var q))
 -> Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
 -> Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q)))
-> [Type (Origin (Src q)) (Name (Var q))]
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Type (Origin (Src q)) (Name (Var q))
aT Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty -> Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
ty { typed'type :: Type (Origin (Src q)) (Name (Var q))
typed'type = Type (Origin (Src q)) (Name (Var q))
aT }) [Type (Origin (Src q)) (Name (Var q))]
argsT ([Typed
    (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
 -> [Typed
       (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))])
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q)
-> [Typed
      (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt
        }

    getCaseType :: CaseAltOf' q (TermOf' q) -> TypeOf' q
    getCaseType :: CaseAltOf' q (TermOf' q) -> Type (Origin (Src q)) (Name (Var q))
getCaseType CaseAlt{[Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
Type (Origin (Src q)) (Name (Var q))
TermOf' q
Origin (Src q)
Name (Var q)
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
caseAlt'rhs :: TermOf' q
caseAlt'constrType :: Type (Origin (Src q)) (Name (Var q))
caseAlt'args :: [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
caseAlt'tag :: Name (Var q)
caseAlt'loc :: Origin (Src q)
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'constrType :: forall loc v a. CaseAlt loc v a -> Type loc v
..} = [Type (Origin (Src q)) (Name (Var q))]
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
funT ((Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
 -> Type (Origin (Src q)) (Name (Var q)))
-> [Typed
      (Origin (Src q)) (Name (Var q)) (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 Typed
  (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v a. Typed loc v a -> Type loc v
typed'type [Typed
   (Origin (Src q)) (Name (Var q)) (Origin (Src q), Name (Var q))]
caseAlt'args) Type (Origin (Src q)) (Name (Var q))
caseAlt'constrType

    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)


    funT :: [TypeOf' q] -> TypeOf' q -> TypeOf' q
    funT :: [Type (Origin (Src q)) (Name (Var q))]
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
funT [Type (Origin (Src q)) (Name (Var q))]
argsT Type (Origin (Src q)) (Name (Var q))
resT = (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))
-> [Type (Origin (Src q)) (Name (Var q))]
-> Type (Origin (Src q)) (Name (Var q))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Type (Origin (Src q)) (Name (Var q))
a Type (Origin (Src q)) (Name (Var q))
b -> 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 (Type (Origin (Src q)) (Name (Var q))
-> Loc (Type (Origin (Src q)) (Name (Var q)))
forall f. HasLoc f => f -> Loc f
getLoc Type (Origin (Src q)) (Name (Var q))
a) Type (Origin (Src q)) (Name (Var q))
a Type (Origin (Src q)) (Name (Var q))
b) Type (Origin (Src q)) (Name (Var q))
resT [Type (Origin (Src q)) (Name (Var q))]
argsT

    applyAlt :: Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst loc v
subst alt :: CaseAlt loc v (f loc v)
alt@CaseAlt{v
loc
f loc v
[Typed loc v (loc, v)]
Type loc v
caseAlt'rhs :: f loc v
caseAlt'constrType :: Type loc v
caseAlt'args :: [Typed loc v (loc, v)]
caseAlt'tag :: v
caseAlt'loc :: loc
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'constrType :: forall loc v a. CaseAlt loc v a -> Type loc v
..} = CaseAlt loc v (f loc v)
alt
      { caseAlt'constrType :: Type loc v
caseAlt'constrType = 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
subst Type loc v
caseAlt'constrType
      , caseAlt'args :: [Typed loc v (loc, v)]
caseAlt'args       = (Typed loc v (loc, v) -> Typed loc v (loc, v))
-> [Typed loc v (loc, v)] -> [Typed loc v (loc, v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Typed loc v (loc, v) -> Typed loc v (loc, v)
applyTyped [Typed loc v (loc, v)]
caseAlt'args
      , 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
caseAlt'rhs
      }
      where
        applyTyped :: Typed loc v (loc, v) -> Typed loc v (loc, v)
applyTyped ty :: Typed loc v (loc, v)
ty@Typed{(loc, v)
Type loc v
typed'value :: (loc, v)
typed'type :: Type loc v
typed'type :: forall loc v a. Typed loc v a -> Type loc v
typed'value :: forall loc v a. Typed loc v a -> a
..} = Typed loc v (loc, v)
ty { typed'type :: Type loc v
typed'type = 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
subst (Type loc v -> Type loc v) -> Type loc v -> Type loc v
forall a b. (a -> b) -> a -> b
$ Type loc v
typed'type }

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, MonadError (TypeError loc (Name v)) m)
  => Subst' loc v
  -> Type' loc v
  -> Type' loc v
  -> m (Subst' loc v)
unify :: Subst' loc v -> Type' loc v -> Type' loc v -> m (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 -> m (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 -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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 -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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 -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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 -> m (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 -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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 -> m (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 -> m (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB = 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) -> 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, MonadError (TypeError loc (Name v)) m)
  => Subst' loc v
  -> [Type' loc v]
  -> [Type' loc v]
  -> m (Subst' loc v)
unifyl :: Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (Subst' loc v)
unifyl Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
 -> m (Subst' loc v) -> m (Subst' loc v))
-> m (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> m (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v) -> m (Subst' loc v) -> m (Subst' loc v)
forall (m :: * -> *) v loc.
(IsVar v, MonadError (TypeError loc (Name v)) m, Show loc) =>
(Type' loc v, Type' loc v) -> m (Subst' loc v) -> m (Subst' loc v)
go (Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)] -> m (Subst' loc v))
-> [(Type' loc v, Type' loc v)] -> m (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) -> m (Subst' loc v) -> m (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) m (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v -> Type' loc v -> Type' loc v -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (Subst' loc v)
unify Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> m (Subst' loc v))
-> m (Subst' loc v) -> m (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (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 (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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, MonadError (TypeError loc (Name v)) m)
  => Subst' loc v
  -> Type' loc v
  -> Type' loc v
  -> m (Subst' loc v)
genSubtypeOf :: Subst' loc v -> Type' loc v -> Type' loc v -> m (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 -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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 -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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] -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (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 -> m (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 -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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 -> m (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 -> m (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 -> m (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB = 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) -> 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, MonadError (TypeError loc (Name v)) m)
  => Subst' loc v
  -> [Type' loc v]
  -> [Type' loc v]
  -> m (Subst' loc v)
subtypeOfL :: Subst' loc v -> [Type' loc v] -> [Type' loc v] -> m (Subst' loc v)
subtypeOfL Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
 -> m (Subst' loc v) -> m (Subst' loc v))
-> m (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> m (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v) -> m (Subst' loc v) -> m (Subst' loc v)
forall (m :: * -> *) v loc.
(IsVar v, MonadError (TypeError loc (Name v)) m, Show loc) =>
(Type' loc v, Type' loc v) -> m (Subst' loc v) -> m (Subst' loc v)
go (Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)] -> m (Subst' loc v))
-> [(Type' loc v, Type' loc v)] -> m (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) -> m (Subst' loc v) -> m (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) m (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v -> Type' loc v -> Type' loc v -> m (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (Subst' loc v)
genSubtypeOf Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> m (Subst' loc v))
-> m (Subst' loc v) -> m (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (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)
unContext 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 r. Bind loc var r -> r
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
$ Map (Name v) (Signature' loc v) -> Context' loc v
forall loc v. Map v (Signature loc v) -> Context loc v
Context (Map (Name v) (Signature' loc v) -> Context' loc v)
-> (Context' loc v -> Map (Name v) (Signature' loc v))
-> Context' loc v
-> Context' loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 r. Bind loc var r -> 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)
unContext (Context' loc v -> Context' loc v)
-> Context' loc v -> Context' 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 (m :: * -> *).
(IsVar v, Show loc, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v -> Type' loc v -> Type' loc v -> m (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
    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 loc v prim.
Ann
  (Type loc (Name v))
  (TermF prim loc (Name v))
  (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v) (Fix (Ann (Type loc v) (TermF prim loc v)))
go Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
x
  where
    go :: Ann
  (Type loc (Name v))
  (TermF prim loc (Name v))
  (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v) (Fix (Ann (Type loc v) (TermF prim loc v)))
go (Ann Type loc (Name v)
annTy TermF prim loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
term) = (Type loc v
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either (TypeError loc v) (Type loc v)
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v) (Fix (Ann (Type loc v) (TermF prim loc v)))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\Type loc v
t TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
val -> Ann
  (Type loc v)
  (TermF prim loc v)
  (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
   (Type loc v)
   (TermF prim loc v)
   (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> Ann
     (Type loc v)
     (TermF prim loc v)
     (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
forall a b. (a -> b) -> a -> b
$ Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Ann
     (Type loc v)
     (TermF prim loc v)
     (Fix (Ann (Type loc v) (TermF prim loc v)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann Type loc v
t TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
val) (Type loc (Name v) -> Either (TypeError loc v) (Type loc v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name v)
annTy) (Either
   (TypeError loc v)
   (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
 -> Either
      (TypeError loc v) (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v) (Fix (Ann (Type loc v) (TermF prim loc v)))
forall a b. (a -> b) -> a -> b
$ case TermF prim loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
term of
      Var loc
loc Name v
v           -> (v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either (TypeError loc v) v
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc
-> v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Var loc
loc) (Either (TypeError loc v) v
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either (TypeError loc v) v
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError loc v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
      Prim loc
loc prim
p          -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ loc
-> prim
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> prim -> TermF prim loc v r
Prim loc
loc prim
p
      App loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
a Fix (Ann (Type loc v) (TermF prim loc v))
b         -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> r -> r -> TermF prim loc v r
App loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
a Fix (Ann (Type loc v) (TermF prim loc v))
b
      Lam loc
loc Name v
v Fix (Ann (Type loc v) (TermF prim loc v))
a         -> (v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either (TypeError loc v) v
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\v
arg -> loc
-> v
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> v -> r -> TermF prim loc v r
Lam loc
loc v
arg Fix (Ann (Type loc v) (TermF prim loc v))
a) (Either (TypeError loc v) v
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either (TypeError loc v) v
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError loc v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
      Let loc
loc Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
bind Fix (Ann (Type loc v) (TermF prim loc v))
a      -> (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
b -> loc
-> Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> Bind loc v r -> r -> TermF prim loc v r
Let loc
loc Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
b Fix (Ann (Type loc v) (TermF prim loc v))
a) (Either
   (TypeError loc v)
   (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either
     (TypeError loc v)
     (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall loc var r loc.
Bind loc (Name var) r
-> Either (TypeError loc var) (Bind loc var r)
fromBind Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
bind
      LetRec loc
loc [Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
binds Fix (Ann (Type loc v) (TermF prim loc v))
a  -> ([Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
bs -> loc
-> [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r.
loc -> [Bind loc v r] -> r -> TermF prim loc v r
LetRec loc
loc [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
bs Fix (Ann (Type loc v) (TermF prim loc v))
a) (Either
   (TypeError loc v)
   [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either
     (TypeError loc v)
     [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ (Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Either
      (TypeError loc v)
      (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> [Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall loc var r loc.
Bind loc (Name var) r
-> Either (TypeError loc var) (Bind loc var r)
fromBind [Bind loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
binds
      AssertType loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
a Type loc (Name v)
ty -> (Type loc v
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either (TypeError loc v) (Type loc v)
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> r -> Type loc v -> TermF prim loc v r
AssertType loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
a) (Either (TypeError loc v) (Type loc v)
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either (TypeError loc v) (Type loc v)
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ Type loc (Name v) -> Either (TypeError loc v) (Type loc v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name v)
ty
      Constr loc
loc Type loc (Name v)
t Name v
v      -> (Type loc v
 -> v
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either (TypeError loc v) (Type loc v)
-> Either (TypeError loc v) v
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (loc
-> Type loc v
-> v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> Type loc v -> v -> TermF prim loc v r
Constr loc
loc) (Type loc (Name v) -> Either (TypeError loc v) (Type loc v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name v)
t) (Name v -> Either (TypeError loc v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v)
      Bottom loc
loc          -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ loc -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> TermF prim loc v r
Bottom loc
loc
      Case loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
e [CaseAlt loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
alts     -> ([CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> Either
     (TypeError loc v)
     [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
e) (Either
   (TypeError loc v)
   [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
 -> Either
      (TypeError loc v)
      (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> Either
     (TypeError loc v)
     [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall a b. (a -> b) -> a -> b
$ (CaseAlt loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Either
      (TypeError loc v)
      (CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))))
-> [CaseAlt
      loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Either
     (TypeError loc v)
     [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Either
     (TypeError loc v)
     (CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
forall loc var a.
CaseAlt loc (Name var) a
-> Either (TypeError loc var) (CaseAlt loc var a)
fromAlt [CaseAlt loc (Name v) (Fix (Ann (Type loc v) (TermF prim loc v)))]
alts

    fromBind :: Bind loc (Name var) r
-> Either (TypeError loc var) (Bind loc var r)
fromBind Bind loc (Name var) r
b = (var -> Bind loc var r)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
a -> Bind loc (Name var) r
b { bind'lhs :: var
bind'lhs = var
a }) (Either (TypeError loc var) var
 -> Either (TypeError loc var) (Bind loc var r))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var r)
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) r -> Name var
forall loc var r. Bind loc var r -> var
bind'lhs Bind loc (Name var) r
b

    fromAlt :: CaseAlt loc (Name var) a
-> Either (TypeError loc var) (CaseAlt loc var a)
fromAlt alt :: CaseAlt loc (Name var) a
alt@CaseAlt{a
loc
[Typed loc (Name var) (loc, Name var)]
Type loc (Name var)
Name var
caseAlt'rhs :: a
caseAlt'constrType :: Type loc (Name var)
caseAlt'args :: [Typed loc (Name var) (loc, Name var)]
caseAlt'tag :: Name var
caseAlt'loc :: loc
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'constrType :: forall loc v a. CaseAlt loc v a -> Type loc v
..} =
      (var
 -> [Typed loc var (loc, var)] -> Type loc var -> CaseAlt loc var a)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) [Typed loc var (loc, var)]
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (CaseAlt loc var a)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (\var
tag [Typed loc var (loc, var)]
args Type loc var
constrType -> CaseAlt loc (Name var) a
alt { caseAlt'tag :: var
caseAlt'tag = var
tag, caseAlt'args :: [Typed loc var (loc, var)]
caseAlt'args = [Typed loc var (loc, var)]
args, caseAlt'constrType :: Type loc var
caseAlt'constrType = Type loc var
constrType })
        (Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
caseAlt'tag)
        ((Typed loc (Name var) (loc, Name var)
 -> Either (TypeError loc var) (Typed loc var (loc, var)))
-> [Typed loc (Name var) (loc, Name var)]
-> Either (TypeError loc var) [Typed loc var (loc, var)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Typed loc (Name var) (loc, Name var)
-> Either (TypeError loc var) (Typed loc var (loc, var))
forall (t :: * -> *) loc v.
Traversable t =>
Typed loc (Name v) (t (Name v))
-> Either (TypeError loc v) (Typed loc v (t v))
fromTyped [Typed loc (Name var) (loc, Name var)]
caseAlt'args)
        (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)
caseAlt'constrType)

    fromTyped :: Typed loc (Name v) (t (Name v))
-> Either (TypeError loc v) (Typed loc v (t v))
fromTyped Typed{t (Name v)
Type loc (Name v)
typed'value :: t (Name v)
typed'type :: Type loc (Name v)
typed'type :: forall loc v a. Typed loc v a -> Type loc v
typed'value :: forall loc v a. Typed loc v a -> a
..} = (Type loc v -> t v -> Typed loc v (t v))
-> Either (TypeError loc v) (Type loc v)
-> Either (TypeError loc v) (t v)
-> Either (TypeError loc v) (Typed loc v (t v))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Type loc v -> t v -> Typed loc v (t v)
forall loc v a. Type loc v -> a -> Typed loc v a
Typed (Type loc (Name v) -> Either (TypeError loc v) (Type loc v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name v)
typed'type) ((Name v -> Either (TypeError loc v) v)
-> t (Name v) -> Either (TypeError loc v) (t v)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name v -> Either (TypeError loc v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar t (Name v)
typed'value)

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