module Type.Check.HM.Infer(
Context(..)
, insertCtx
, lookupCtx
, insertConstructorCtx
, lookupConstructorCtx
, ContextOf
, inferType
, inferTerm
, inferTypeList
, inferTermList
, subtypeOf
, unifyTypes
, closeSignature
, printInfer
) where
import Control.Monad.Identity
import Control.Monad.Writer.Strict
import Control.Applicative
import Control.Arrow (second)
import Control.Monad.Except
import Control.Monad.State.Strict
import Data.Bifunctor (bimap)
import Data.Fix
import Data.Function (on)
import Data.Map.Strict (Map)
import Data.Maybe
import Type.Check.HM.Lang
import Type.Check.HM.Term
import Type.Check.HM.Subst
import Type.Check.HM.Type
import Type.Check.HM.TypeError
import Type.Check.HM.TyTerm
import Type.Check.HM.Pretty
import qualified Data.Map.Strict as M
import qualified Data.Set as S
import qualified Data.List as L
data Context loc v = Context
{ Context loc v -> Map v (Signature loc v)
context'binds :: Map v (Signature loc v)
, Context loc v -> Map v (Signature loc v)
context'constructors :: 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)
instance Ord v => Semigroup (Context loc v) where
<> :: Context loc v -> Context loc v -> Context loc v
(<>) (Context Map v (Signature loc v)
bs1 Map v (Signature loc v)
cs1) (Context Map v (Signature loc v)
bs2 Map v (Signature loc v)
cs2) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v)
bs1 Map v (Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a. Semigroup a => a -> a -> a
<> Map v (Signature loc v)
bs2) (Map v (Signature loc v)
cs1 Map v (Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a. Semigroup a => a -> a -> a
<> Map v (Signature loc v)
cs2)
instance Ord v => Monoid (Context loc v) where
mempty :: Context loc v
mempty = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context Map v (Signature loc v)
forall a. Monoid a => a
mempty Map v (Signature loc v)
forall a. Monoid a => a
mempty
type ContextOf q = Context (Src q) (Var q)
instance CanApply Context where
apply :: Subst loc v -> Context loc v -> Context loc v
apply Subst loc v
subst Context loc v
ctx = Context loc v
ctx
{ context'binds :: Map v (Signature loc v)
context'binds = (Signature loc v -> Signature loc v)
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst loc v -> Signature loc v -> Signature loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
subst) (Map v (Signature loc v) -> Map v (Signature loc v))
-> Map v (Signature loc v) -> Map v (Signature loc v)
forall a b. (a -> b) -> a -> b
$ Context loc v -> Map v (Signature loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds Context loc v
ctx
}
insertCtx :: Ord v => v -> Signature loc v -> Context loc v -> Context loc v
insertCtx :: v -> Signature loc v -> Context loc v -> Context loc v
insertCtx v
v Signature loc v
sign (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (v
-> Signature loc v
-> Map v (Signature loc v)
-> Map v (Signature loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Signature loc v
sign Map v (Signature loc v)
binds) Map v (Signature loc v)
cons
lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
lookupCtx :: v -> Context loc v -> Maybe (Signature loc v)
lookupCtx v
v (Context Map v (Signature loc v)
binds Map v (Signature loc v)
_cons) = v -> Map v (Signature loc v) -> Maybe (Signature loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Signature loc v)
binds
insertConstructorCtx :: Ord v => v -> Signature loc v -> Context loc v -> Context loc v
insertConstructorCtx :: v -> Signature loc v -> Context loc v -> Context loc v
insertConstructorCtx v
v Signature loc v
sign (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context Map v (Signature loc v)
binds (v
-> Signature loc v
-> Map v (Signature loc v)
-> Map v (Signature loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Signature loc v
sign Map v (Signature loc v)
cons)
lookupConstructorCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx :: v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx v
v (Context Map v (Signature loc v)
_binds Map v (Signature loc v)
cons) = v -> Map v (Signature loc v) -> Maybe (Signature loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Signature loc v)
cons
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])
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))
restrictContext :: Ord v => Term prim loc v -> Context loc v -> Context loc v
restrictContext :: Term prim loc v -> Context loc v -> Context loc v
restrictContext Term prim loc v
t (Context Map v (Signature loc v)
binds Map v (Signature loc v)
cons) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Map v () -> Map v (Signature loc v)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.intersection Map v (Signature loc v)
binds Map v ()
fv) Map v (Signature loc v)
cons
where
fv :: Map v ()
fv = [(v, ())] -> Map v ()
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(v, ())] -> Map v ()) -> [(v, ())] -> Map v ()
forall a b. (a -> b) -> a -> b
$ (v -> (v, ())) -> [v] -> [(v, ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, ()) ([v] -> [(v, ())]) -> [v] -> [(v, ())]
forall a b. (a -> b) -> a -> b
$ Set v -> [v]
forall a. Set a -> [a]
S.toList (Set v -> [v]) -> Set v -> [v]
forall a b. (a -> b) -> a -> b
$ Term prim loc v -> Set v
forall v prim loc. Ord v => Term prim loc v -> Set v
freeVars Term prim loc v
t
wrapContextNames :: Ord v => Context loc v -> Context loc (Name v)
wrapContextNames :: Context loc v -> Context loc (Name v)
wrapContextNames = (v -> Name v) -> Context loc v -> Context loc (Name v)
forall v k1 loc.
Ord v =>
(k1 -> v) -> Context loc k1 -> Context loc v
fmapCtx v -> Name v
forall v. v -> Name v
Name
where
fmapCtx :: (k1 -> v) -> Context loc k1 -> Context loc v
fmapCtx k1 -> v
f (Context Map k1 (Signature loc k1)
bs Map k1 (Signature loc k1)
cs) = Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap Map k1 (Signature loc k1)
bs) (Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap Map k1 (Signature loc k1)
cs)
where
wrap :: Map k1 (Signature loc k1) -> Map v (Signature loc v)
wrap = (k1 -> v) -> Map k1 (Signature loc v) -> Map v (Signature loc v)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys k1 -> v
f (Map k1 (Signature loc v) -> Map v (Signature loc v))
-> (Map k1 (Signature loc k1) -> Map k1 (Signature loc v))
-> Map k1 (Signature loc k1)
-> Map v (Signature loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signature loc k1 -> Signature loc v)
-> Map k1 (Signature loc k1) -> Map k1 (Signature loc v)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((k1 -> v) -> Signature loc k1 -> Signature loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap k1 -> v
f)
wrapTermNames :: Term prim loc v -> Term prim loc (Name v)
wrapTermNames :: Term prim loc v -> Term prim loc (Name v)
wrapTermNames = (v -> Name v) -> Term prim loc v -> Term prim loc (Name v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name
markProven :: Context loc v -> Context (Origin loc) v
markProven :: Context loc v -> Context (Origin loc) v
markProven (Context Map v (Signature loc v)
bs Map v (Signature loc v)
cs) = Map v (Signature (Origin loc) v)
-> Map v (Signature (Origin loc) v) -> Context (Origin loc) v
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context (Map v (Signature loc v) -> Map v (Signature (Origin loc) v)
forall k a var.
Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark Map v (Signature loc v)
bs) (Map v (Signature loc v) -> Map v (Signature (Origin loc) v)
forall k a var.
Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark Map v (Signature loc v)
cs)
where
mark :: Map k (Signature a var) -> Map k (Signature (Origin a) var)
mark = (Signature a var -> Signature (Origin a) var)
-> Map k (Signature a var) -> Map k (Signature (Origin a) var)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((a -> Origin a) -> Signature a var -> Signature (Origin a) var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc a -> Origin a
forall a. a -> Origin a
Proven)
markUserCode :: Term prim loc v -> Term prim (Origin loc) v
markUserCode :: Term prim loc v -> Term prim (Origin loc) v
markUserCode = (loc -> Origin loc) -> Term prim loc v -> Term prim (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode
chooseUserOrigin :: Show a => Origin a -> Origin a -> a
chooseUserOrigin :: Origin a -> Origin a -> a
chooseUserOrigin Origin a
x Origin a
y = case (Origin a
x, Origin a
y) of
(UserCode a
a, Origin a
_) -> a
a
(Origin a
_, UserCode a
a) -> a
a
(Origin a, Origin a)
_ -> Origin a -> a
forall a. Origin a -> a
fromOrigin Origin a
x
data Origin a
= Proven a
| UserCode a
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
newtype InferM loc var a = InferM (StateT Int (Writer [TypeError loc (Name var)]) a)
deriving (a -> InferM loc var b -> InferM loc var a
(a -> b) -> InferM loc var a -> InferM loc var b
(forall a b. (a -> b) -> InferM loc var a -> InferM loc var b)
-> (forall a b. a -> InferM loc var b -> InferM loc var a)
-> Functor (InferM loc var)
forall a b. a -> InferM loc var b -> InferM loc var a
forall a b. (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a b. a -> InferM loc var b -> InferM loc var a
forall loc var a b.
(a -> b) -> InferM loc var a -> InferM loc var b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> InferM loc var b -> InferM loc var a
$c<$ :: forall loc var a b. a -> InferM loc var b -> InferM loc var a
fmap :: (a -> b) -> InferM loc var a -> InferM loc var b
$cfmap :: forall loc var a b.
(a -> b) -> InferM loc var a -> InferM loc var b
Functor, Functor (InferM loc var)
a -> InferM loc var a
Functor (InferM loc var)
-> (forall a. a -> InferM loc var a)
-> (forall a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b)
-> (forall a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c)
-> (forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b)
-> (forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var a)
-> Applicative (InferM loc var)
InferM loc var a -> InferM loc var b -> InferM loc var b
InferM loc var a -> InferM loc var b -> InferM loc var a
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall a. a -> InferM loc var a
forall loc var. Functor (InferM loc var)
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a. a -> InferM loc var a
forall a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall loc var a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
forall loc var a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: InferM loc var a -> InferM loc var b -> InferM loc var a
$c<* :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var a
*> :: InferM loc var a -> InferM loc var b -> InferM loc var b
$c*> :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
liftA2 :: (a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
$cliftA2 :: forall loc var a b c.
(a -> b -> c)
-> InferM loc var a -> InferM loc var b -> InferM loc var c
<*> :: InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
$c<*> :: forall loc var a b.
InferM loc var (a -> b) -> InferM loc var a -> InferM loc var b
pure :: a -> InferM loc var a
$cpure :: forall loc var a. a -> InferM loc var a
$cp1Applicative :: forall loc var. Functor (InferM loc var)
Applicative, Applicative (InferM loc var)
a -> InferM loc var a
Applicative (InferM loc var)
-> (forall a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b)
-> (forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b)
-> (forall a. a -> InferM loc var a)
-> Monad (InferM loc var)
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a. a -> InferM loc var a
forall loc var. Applicative (InferM loc var)
forall a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
forall loc var a. a -> InferM loc var a
forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
forall loc var a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> InferM loc var a
$creturn :: forall loc var a. a -> InferM loc var a
>> :: InferM loc var a -> InferM loc var b -> InferM loc var b
$c>> :: forall loc var a b.
InferM loc var a -> InferM loc var b -> InferM loc var b
>>= :: InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
$c>>= :: forall loc var a b.
InferM loc var a -> (a -> InferM loc var b) -> InferM loc var b
$cp1Monad :: forall loc var. Applicative (InferM loc var)
Monad, MonadState Int, MonadWriter [TypeError loc (Name var)])
runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM (InferM StateT Int (Writer [TypeError loc (Name var)]) a
m) = case Writer [TypeError loc (Name var)] a
-> (a, [TypeError loc (Name var)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [TypeError loc (Name var)] a
-> (a, [TypeError loc (Name var)]))
-> Writer [TypeError loc (Name var)] a
-> (a, [TypeError loc (Name var)])
forall a b. (a -> b) -> a -> b
$ StateT Int (Writer [TypeError loc (Name var)]) a
-> Int -> Writer [TypeError loc (Name var)] a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT Int (Writer [TypeError loc (Name var)]) a
m Int
0 of
(a
res, []) -> a -> Either [TypeError loc (Name var)] a
forall a b. b -> Either a b
Right a
res
(a
_, [TypeError loc (Name var)]
errs) -> [TypeError loc (Name var)] -> Either [TypeError loc (Name var)] a
forall a b. a -> Either a b
Left [TypeError loc (Name var)]
errs
type InferOf q = InferM (Src q) (Var q) (Out (Prim q) (Src q) (Var q))
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
inferTerm :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm :: ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm ContextOf q
ctx TermOf q
term =
case InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either
[TypeError (Src q) (Name (Var q))]
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall loc var a.
InferM loc var a -> Either [TypeError loc (Name var)] a
runInferM (InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either
[TypeError (Src q) (Name (Var q))]
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> Either
[TypeError (Src q) (Name (Var q))]
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ ContextOf' q
-> TermOf' q
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer (Context (Origin (Src q)) (Var q) -> ContextOf' q
forall v loc. Ord v => Context loc v -> Context loc (Name v)
wrapContextNames (Context (Origin (Src q)) (Var q) -> ContextOf' q)
-> Context (Origin (Src q)) (Var q) -> ContextOf' q
forall a b. (a -> b) -> a -> b
$ ContextOf q -> Context (Origin (Src q)) (Var q)
forall loc v. Context loc v -> Context (Origin loc) v
markProven (ContextOf q -> Context (Origin (Src q)) (Var q))
-> ContextOf q -> Context (Origin (Src q)) (Var q)
forall a b. (a -> b) -> a -> b
$ TermOf q -> ContextOf q -> ContextOf q
forall v prim loc.
Ord v =>
Term prim loc v -> Context loc v -> Context loc v
restrictContext TermOf q
term ContextOf q
ctx) (Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q
forall prim loc v. Term prim loc v -> Term prim loc (Name v)
wrapTermNames (Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q)
-> Term (Prim q) (Origin (Src q)) (Var q) -> TermOf' q
forall a b. (a -> b) -> a -> b
$ TermOf q -> Term (Prim q) (Origin (Src q)) (Var q)
forall prim loc v. Term prim loc v -> Term prim (Origin loc) v
markUserCode TermOf q
term) of
Right (Subst (Origin (Src q)) (Name (Var q))
_, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTerm) -> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTermOf q)
forall prim.
TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
toTyTerm TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTerm
Left [TypeError (Src q) (Name (Var q))]
errs -> [ErrorOf q] -> Either [ErrorOf q] (TyTermOf q)
forall a b. a -> Either a b
Left ([ErrorOf q] -> Either [ErrorOf q] (TyTermOf q))
-> [ErrorOf q] -> Either [ErrorOf q] (TyTermOf q)
forall a b. (a -> b) -> a -> b
$ (TypeError (Src q) (Name (Var q)) -> ErrorOf q)
-> [TypeError (Src q) (Name (Var q))] -> [ErrorOf q]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeError (Src q) (Name (Var q)) -> ErrorOf q
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError (Src q) (Name (Var q)) -> ErrorOf q)
-> (TypeError (Src q) (Name (Var q))
-> TypeError (Src q) (Name (Var q)))
-> TypeError (Src q) (Name (Var q))
-> ErrorOf q
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError (Src q) (Name (Var q))
-> TypeError (Src q) (Name (Var q))
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) [TypeError (Src q) (Name (Var q))]
errs
where
toTyTerm :: TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
toTyTerm = (ErrorOf q -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Src q) (Var q)
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([ErrorOf q] -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a b. a -> Either a b
Left ([ErrorOf q] -> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (ErrorOf q -> [ErrorOf q])
-> ErrorOf q
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorOf q -> [ErrorOf q]
forall (f :: * -> *) a. Applicative f => a -> f a
pure) TyTerm prim (Src q) (Var q)
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall a b. b -> Either a b
Right (Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either [ErrorOf q] (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyTerm prim (Src q) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
forall prim loc var.
TyTerm prim loc (Name var)
-> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar (TyTerm prim (Src q) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> Either (ErrorOf q) (TyTerm prim (Src q) (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyTerm prim (Src q) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType (TyTerm prim (Src q) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q)))
-> (TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q)))
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Origin (Src q) -> Src q)
-> TyTerm prim (Origin (Src q)) (Name (Var q))
-> TyTerm prim (Src q) (Name (Var q))
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin
type Out prim loc var = ( Subst (Origin loc) (Name var)
, TyTerm prim (Origin loc) (Name var)
)
inferTermList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList :: ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs = case [Bind (Src q) (Var q) (TermOf q)]
defs of
[] -> [Bind (Src q) (Var q) (TyTermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Bind (Src q) (Var q) (TermOf q)
d:[Bind (Src q) (Var q) (TermOf q)]
_ ->
let topLoc :: Src q
topLoc = Bind (Src q) (Var q) (TermOf q) -> Src q
forall loc var a. Bind loc var a -> loc
bind'loc Bind (Src q) (Var q) (TermOf q)
d
in (TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)])
-> Either [ErrorOf q] (TyTermOf q)
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)]
fromLetExpr (Either [ErrorOf q] (TyTermOf q)
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)])
-> Either [ErrorOf q] (TyTermOf q)
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
forall a b. (a -> b) -> a -> b
$ ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
forall q.
Lang q =>
ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
inferTerm ContextOf q
ctx (Src q -> [Bind (Src q) (Var q) (TermOf q)] -> TermOf q
forall loc v prim.
loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v
toLetExpr Src q
topLoc [Bind (Src q) (Var q) (TermOf q)]
defs)
where
toLetExpr :: loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v
toLetExpr loc
loc [Bind loc v (Term prim loc v)]
ds = loc
-> [Bind loc v (Term prim loc v)]
-> Term prim loc v
-> Term prim loc v
forall loc v prim.
loc
-> [Bind loc v (Term prim loc v)]
-> Term prim loc v
-> Term prim loc v
letRecE loc
loc ((Bind loc v (Term prim loc v) -> Bind loc v (Term prim loc v))
-> [Bind loc v (Term prim loc v)] -> [Bind loc v (Term prim loc v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bind loc v (Term prim loc v) -> Bind loc v (Term prim loc v)
forall a. a -> a
toBind [Bind loc v (Term prim loc v)]
ds) (loc -> Term prim loc v
forall loc prim v. loc -> Term prim loc v
bottomE loc
loc)
fromLetExpr :: TyTermOf q -> [Bind (Src q) (Var q) (TyTermOf q)]
fromLetExpr = \case
(TyTerm (Fix (Ann Type (Src q) (Var q)
_ (LetRec Src q
_ [Bind
(Src q)
(Var q)
(Fix
(Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
bs Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q)))
_)))) -> (Bind
(Src q)
(Var q)
(Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))
-> Bind (Src q) (Var q) (TyTermOf q))
-> [Bind
(Src q)
(Var q)
(Fix
(Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
-> [Bind (Src q) (Var q) (TyTermOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bind
(Src q)
(Var q)
(Fix (Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))
-> Bind (Src q) (Var q) (TyTermOf q)
forall loc v prim.
Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
fromBind [Bind
(Src q)
(Var q)
(Fix
(Ann (Type (Src q) (Var q)) (TermF (Prim q) (Src q) (Var q))))]
bs
TyTermOf q
_ -> String -> [Bind (Src q) (Var q) (TyTermOf q)]
forall a. HasCallStack => String -> a
error String
"Imposible happened. Found non let-rec expression"
toBind :: a -> a
toBind = a -> a
forall a. a -> a
id
fromBind :: Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
fromBind = (Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v)
-> Bind (Src q) (Var q) (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind (Src q) (Var q) (TyTerm prim loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm
inferTypeList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
inferTypeList :: ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
inferTypeList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs = ([Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> [Bind (Src q) (Var q) (TypeOf q)])
-> Either
[ErrorOf q]
[Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))
-> Bind (Src q) (Var q) (TypeOf q))
-> [Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> [Bind (Src q) (Var q) (TypeOf q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyTerm (Prim q) (Src q) (Var q) -> TypeOf q)
-> Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))
-> Bind (Src q) (Var q) (TypeOf q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm (Prim q) (Src q) (Var q) -> TypeOf q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType)) (Either
[ErrorOf q]
[Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)])
-> Either
[ErrorOf q]
[Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
forall a b. (a -> b) -> a -> b
$ ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either
[ErrorOf q]
[Bind (Src q) (Var q) (TyTerm (Prim q) (Src q) (Var q))]
forall q.
Lang q =>
ContextOf q
-> [Bind (Src q) (Var q) (TermOf q)]
-> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
inferTermList ContextOf q
ctx [Bind (Src q) (Var q) (TermOf q)]
defs
infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer :: ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx (Term (Fix TermF
(Prim q)
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
x)) = case TermF
(Prim q)
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
x of
Var Origin (Src q)
loc Name (Var q)
v -> ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
forall q.
Lang q =>
ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v
Prim Origin (Src q)
loc Prim q
p -> Origin (Src q) -> Prim q -> InferOf q
forall q. Lang q => Origin (Src q) -> Prim q -> InferOf q
inferPrim Origin (Src q)
loc Prim q
p
App Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
b -> ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
b)
Lam Origin (Src q)
loc Name (Var q)
v Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
r -> ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
r)
Let Origin (Src q)
loc Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
v Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a -> ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
inferLet ContextOf' q
ctx Origin (Src q)
loc ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> BindOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
v) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a)
LetRec Origin (Src q)
loc [Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
vs Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a -> ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
inferLetRec ContextOf' q
ctx Origin (Src q)
loc ((Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> BindOf' q (TermOf' q))
-> [Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
-> [BindOf' q (TermOf' q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> BindOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term) [Bind
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
vs) (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a)
AssertType Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a Type (Origin (Src q)) (Name (Var q))
ty -> ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> Type (Origin (Src q)) (Name (Var q))
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
a) Type (Origin (Src q)) (Name (Var q))
ty
Constr Origin (Src q)
loc Name (Var q)
tag -> ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
forall q.
Lang q =>
ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
tag
Case Origin (Src q)
loc Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
e [CaseAlt
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
alts -> ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
forall q.
Lang q =>
ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
inferCase ContextOf' q
ctx Origin (Src q)
loc (Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q)))
e) ((CaseAlt
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> CaseAltOf' q (TermOf' q))
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
-> [CaseAltOf' q (TermOf' q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q)
-> CaseAlt
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))
-> CaseAltOf' q (TermOf' q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))) -> TermOf' q
forall prim loc v. Fix (TermF prim loc v) -> Term prim loc v
Term) [CaseAlt
(Origin (Src q))
(Name (Var q))
(Fix (TermF (Prim q) (Origin (Src q)) (Name (Var q))))]
alts)
Bottom Origin (Src q)
loc -> Origin (Src q) -> InferOf q
forall q. Lang q => Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc
retryWithBottom :: Lang q => TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom :: TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc = do
[TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
Origin (Src q) -> InferOf q
forall q. Lang q => Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc
inferVar :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar :: ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferVar ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
v =
case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupCtx Name (Var q)
v ContextOf' q
ctx of
Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Name (Var q)
v) Origin (Src q)
loc
Just Signature (Origin (Src q)) (Name (Var q))
sig -> do Type (Origin (Src q)) (Name (Var q))
ty <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance (Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q))))
-> Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Origin (Src q)
-> Signature (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) loc locA v.
LocFunctor f =>
loc -> f locA v -> f loc v
setLoc Origin (Src q)
loc Signature (Origin (Src q)) (Name (Var q))
sig
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc var prim.
Type loc var -> loc -> var -> TyTerm prim loc var
tyVarE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Name (Var q)
v)
inferPrim :: Lang q => Origin (Src q) -> Prim q -> InferOf q
inferPrim :: Origin (Src q) -> Prim q -> InferOf q
inferPrim Origin (Src q)
loc Prim q
prim =
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Prim q
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc var prim.
Type loc var -> loc -> prim -> TyTerm prim loc var
tyPrimE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Prim q
prim)
where
ty :: Type (Origin (Src q)) (Name (Var q))
ty = (Var q -> Name (Var q))
-> Type (Origin (Src q)) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var q -> Name (Var q)
forall v. v -> Name v
Name (Type (Origin (Src q)) (Var q)
-> Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ (Src q -> Origin (Src q))
-> Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Src q -> Origin (Src q)
forall a. a -> Origin a
UserCode (Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q))
-> Type (Src q) (Var q) -> Type (Origin (Src q)) (Var q)
forall a b. (a -> b) -> a -> b
$ Src q -> Prim q -> Type (Src q) (Var q)
forall q. Lang q => Src q -> Prim q -> TypeOf q
getPrimType (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Prim q
prim
inferApp :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp :: ContextOf' q
-> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
inferApp ContextOf' q
ctx Origin (Src q)
loc TermOf' q
f TermOf' q
a = do
Type (Origin (Src q)) (Name (Var q))
tvn <- (Name (Var q) -> Type (Origin (Src q)) (Name (Var q)))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc) (InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q))))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
(Subst' (Src q) (Var q),
[(Type (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
res <- ContextOf' q
-> [TermOf' q]
-> InferM
(Src q)
(Var q)
(Subst' (Src q) (Var q),
[(Type (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms ContextOf' q
ctx [TermOf' q
f, TermOf' q
a]
case (Subst' (Src q) (Var q),
[(Type (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
res of
(Subst' (Src q) (Var q)
phi, [(Type (Origin (Src q)) (Name (Var q))
tf, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
f'), (Type (Origin (Src q)) (Name (Var q))
ta, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
a')]) -> case Subst' (Src q) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
(TypeError (Src q) (Name (Var q))) (Subst' (Src q) (Var q))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' (Src q) (Var q)
phi Type (Origin (Src q)) (Name (Var q))
tf (Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v. loc -> Type loc v -> Type loc v -> Type loc v
arrowT Origin (Src q)
loc Type (Origin (Src q)) (Name (Var q))
ta Type (Origin (Src q)) (Name (Var q))
tvn) of
Left TypeError (Src q) (Name (Var q))
err -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc
Right Subst' (Src q) (Var q)
subst -> let ty :: Type (Origin (Src q)) (Name (Var q))
ty = Subst' (Src q) (Var q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst Type (Origin (Src q)) (Name (Var q))
tvn
term :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
term = Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> TyTerm prim loc v
-> TyTerm prim loc v
-> TyTerm prim loc v
tyAppE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc (Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
f') (Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
a')
in (Subst' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst' (Src q) (Var q)
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
term)
(Subst' (Src q) (Var q),
[(Type (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
_ -> String -> InferOf q
forall a. HasCallStack => String -> a
error String
"Impossible has happened!"
inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam :: ContextOf' q
-> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
inferLam ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
x TermOf' q
body = do
Name (Var q)
tvn <- InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
(Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer (Name (Var q) -> ContextOf' q
ctx1 Name (Var q)
tvn) TermOf' q
body
let ty :: Type (Origin (Src q)) (Name (Var q))
ty = Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall loc v. loc -> Type loc v -> Type loc v -> Type loc v
arrowT Origin (Src q)
loc (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
phi (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc Name (Var q)
tvn)) (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm)
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
phi, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v
tyLamE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc Name (Var q)
x TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTyTerm)
where
ctx1 :: Name (Var q) -> ContextOf' q
ctx1 Name (Var q)
tvn = Name (Var q)
-> Signature (Origin (Src q)) (Name (Var q))
-> ContextOf' q
-> ContextOf' q
forall v loc.
Ord v =>
v -> Signature loc v -> Context loc v -> Context loc v
insertCtx Name (Var q)
x (Origin (Src q)
-> Name (Var q) -> Signature (Origin (Src q)) (Name (Var q))
forall loc v. loc -> v -> Signature loc v
newVar Origin (Src q)
loc Name (Var q)
tvn) ContextOf' q
ctx
inferLet :: Lang q => ContextOf' q -> Origin (Src q) -> BindOf' q (TermOf' q) -> TermOf' q -> InferOf q
inferLet :: ContextOf' q
-> Origin (Src q)
-> BindOf' q (TermOf' q)
-> TermOf' q
-> InferOf q
inferLet ContextOf' q
ctx Origin (Src q)
loc BindOf' q (TermOf' q)
v TermOf' q
body = do
(Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx (TermOf' q -> InferOf q) -> TermOf' q -> InferOf q
forall a b. (a -> b) -> a -> b
$ BindOf' q (TermOf' q) -> TermOf' q
forall loc var a. Bind loc var a -> a
bind'rhs BindOf' q (TermOf' q)
v
let tBind :: Type (Origin (Src q)) (Name (Var q))
tBind = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm
ContextOf' q
ctx1 <- [Bind
(Origin (Src q))
(Name (Var q))
(Type (Origin (Src q)) (Name (Var q)))]
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall v loc.
IsVar v =>
[Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls [(TermOf' q -> Type (Origin (Src q)) (Name (Var q)))
-> BindOf' q (TermOf' q)
-> Bind
(Origin (Src q))
(Name (Var q))
(Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type (Origin (Src q)) (Name (Var q))
-> TermOf' q -> Type (Origin (Src q)) (Name (Var q))
forall a b. a -> b -> a
const Type (Origin (Src q)) (Name (Var q))
tBind) BindOf' q (TermOf' q)
v] (Subst (Origin (Src q)) (Name (Var q))
-> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
phi ContextOf' q
ctx)
(Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 TermOf' q
body
let subst1 :: Subst (Origin (Src q)) (Name (Var q))
subst1 = Subst (Origin (Src q)) (Name (Var q))
phi Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
subst
tyBind :: Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
tyBind = BindOf' q (TermOf' q)
v { bind'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bind'rhs = Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhsTyTerm }
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return ( Subst (Origin (Src q)) (Name (Var q))
subst1
, Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> Bind loc v (TyTerm prim loc v)
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetE (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) Origin (Src q)
loc Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
tyBind TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm
)
inferLetRec :: forall q . Lang q
=> ContextOf' q -> Origin (Src q) -> [BindOf' q (TermOf' q)] -> TermOf' q
-> InferOf q
inferLetRec :: ContextOf' q
-> Origin (Src q)
-> [BindOf' q (TermOf' q)]
-> TermOf' q
-> InferOf q
inferLetRec ContextOf' q
ctx Origin (Src q)
topLoc [BindOf' q (TermOf' q)]
vs TermOf' q
body = do
[(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx <- [BindOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
[(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
getTypesLhs [BindOf' q (TermOf' q)]
vs
(Subst (Origin (Src q)) (Name (Var q))
phi, [(Type' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
rhsTyTerms) <- ContextOf' q
-> [TermOf' q]
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
[(Type' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms (ContextOf' q
ctx ContextOf' q -> ContextOf' q -> ContextOf' q
forall a. Semigroup a => a -> a -> a
<> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> ContextOf' q
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx) Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a. Monoid a => a
mempty) [TermOf' q]
exprBinds
let ([Type' (Src q) (Var q)]
tBinds, [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
bindsTyTerms) = [(Type' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> ([Type' (Src q) (Var q)],
[TyTerm (Prim q) (Origin (Src q)) (Name (Var q))])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
rhsTyTerms
case ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> [Type' (Src q) (Var q)]
-> Either
(TypeError (Src q) (Name (Var q)))
(ContextOf' q,
[(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))],
Subst (Origin (Src q)) (Name (Var q)))
forall v (f :: * -> * -> *) loc a.
(CanApply f, IsVar v, Show loc) =>
f (Origin loc) (Name v)
-> [(a, Signature (Origin loc) (Name v))]
-> Subst (Origin loc) (Name v)
-> [Type' loc v]
-> Either
(TypeError loc (Name v))
(f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v))
unifyRhs ContextOf' q
ctx [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx Subst (Origin (Src q)) (Name (Var q))
phi [Type' (Src q) (Var q)]
tBinds of
Right (ContextOf' q
ctx1, [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx1, Subst (Origin (Src q)) (Name (Var q))
subst) -> [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> TermOf' q
-> InferOf q
inferBody [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
bindsTyTerms ContextOf' q
ctx1 [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx1 Subst (Origin (Src q)) (Name (Var q))
subst TermOf' q
body
Left TypeError (Src q) (Name (Var q))
err -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
topLoc
where
exprBinds :: [TermOf' q]
exprBinds = (BindOf' q (TermOf' q) -> TermOf' q)
-> [BindOf' q (TermOf' q)] -> [TermOf' q]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindOf' q (TermOf' q) -> TermOf' q
forall loc var a. Bind loc var a -> a
bind'rhs [BindOf' q (TermOf' q)]
vs
locBinds :: [Origin (Src q)]
locBinds = (BindOf' q (TermOf' q) -> Origin (Src q))
-> [BindOf' q (TermOf' q)] -> [Origin (Src q)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindOf' q (TermOf' q) -> Origin (Src q)
forall loc var a. Bind loc var a -> loc
bind'loc [BindOf' q (TermOf' q)]
vs
getTypesLhs :: [BindOf' q (TermOf' q)] -> InferM (Src q) (Var q) [(Name (Var q), SignatureOf' q)]
getTypesLhs :: [BindOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
[(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
getTypesLhs [BindOf' q (TermOf' q)]
lhs = (BindOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> [BindOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
[(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\BindOf' q (TermOf' q)
b -> (Name (Var q)
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM
(Src q)
(Var q)
(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BindOf' q (TermOf' q) -> Name (Var q)
forall loc var a. Bind loc var a -> var
bind'lhs BindOf' q (TermOf' q)
b, ) (Signature (Origin (Src q)) (Name (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> (Name (Var q) -> Signature (Origin (Src q)) (Name (Var q)))
-> Name (Var q)
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Origin (Src q)
-> Name (Var q) -> Signature (Origin (Src q)) (Name (Var q))
forall loc v. loc -> v -> Signature loc v
newVar (BindOf' q (TermOf' q) -> Origin (Src q)
forall loc var a. Bind loc var a -> loc
bind'loc BindOf' q (TermOf' q)
b)) InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar) [BindOf' q (TermOf' q)]
lhs
unifyRhs :: f (Origin loc) (Name v)
-> [(a, Signature (Origin loc) (Name v))]
-> Subst (Origin loc) (Name v)
-> [Type' loc v]
-> Either
(TypeError loc (Name v))
(f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v))
unifyRhs f (Origin loc) (Name v)
context [(a, Signature (Origin loc) (Name v))]
lhsCtx Subst (Origin loc) (Name v)
phi [Type' loc v]
tBinds =
(Subst (Origin loc) (Name v)
-> (f (Origin loc) (Name v),
[(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc (Name v))
(f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Subst (Origin loc) (Name v)
subst -> (f (Origin loc) (Name v)
context1, [(a, Signature (Origin loc) (Name v))]
lhsCtx1, Subst (Origin loc) (Name v)
subst)) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc (Name v))
(f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc (Name v))
(f (Origin loc) (Name v), [(a, Signature (Origin loc) (Name v))],
Subst (Origin loc) (Name v))
forall a b. (a -> b) -> a -> b
$ Subst (Origin loc) (Name v)
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst (Origin loc) (Name v)
phi [Type' loc v]
ts [Type' loc v]
tBinds
where
context1 :: f (Origin loc) (Name v)
context1 = Subst (Origin loc) (Name v)
-> f (Origin loc) (Name v) -> f (Origin loc) (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
phi f (Origin loc) (Name v)
context
lhsCtx1 :: [(a, Signature (Origin loc) (Name v))]
lhsCtx1 = ((a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v)))
-> [(a, Signature (Origin loc) (Name v))]
-> [(a, Signature (Origin loc) (Name v))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Signature (Origin loc) (Name v)
-> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Signature (Origin loc) (Name v)
-> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v)))
-> (Signature (Origin loc) (Name v)
-> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
forall a b. (a -> b) -> a -> b
$ Subst (Origin loc) (Name v)
-> Signature (Origin loc) (Name v)
-> Signature (Origin loc) (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
phi) [(a, Signature (Origin loc) (Name v))]
lhsCtx
ts :: [Type' loc v]
ts = ((a, Signature (Origin loc) (Name v)) -> Type' loc v)
-> [(a, Signature (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Signature (Origin loc) (Name v) -> Type' loc v
forall loc var. Signature loc var -> Type loc var
oldBvar (Signature (Origin loc) (Name v) -> Type' loc v)
-> ((a, Signature (Origin loc) (Name v))
-> Signature (Origin loc) (Name v))
-> (a, Signature (Origin loc) (Name v))
-> Type' loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Signature (Origin loc) (Name v))
-> Signature (Origin loc) (Name v)
forall a b. (a, b) -> b
snd) [(a, Signature (Origin loc) (Name v))]
lhsCtx1
oldBvar :: Signature loc var -> Type loc var
oldBvar = (SignatureF loc var (Type loc var) -> Type loc var)
-> Fix (SignatureF loc var) -> Type loc var
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix SignatureF loc var (Type loc var) -> Type loc var
forall loc var. SignatureF loc var (Type loc var) -> Type loc var
go (Fix (SignatureF loc var) -> Type loc var)
-> (Signature loc var -> Fix (SignatureF loc var))
-> Signature loc var
-> Type loc var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature loc var -> Fix (SignatureF loc var)
forall loc var. Signature loc var -> Fix (SignatureF loc var)
unSignature
where
go :: SignatureF loc var (Type loc var) -> Type loc var
go = \case
MonoT Type loc var
t -> Type loc var
t
ForAllT loc
_ var
_ Type loc var
t -> Type loc var
t
inferBody :: [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> ContextOf' q
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Subst (Origin (Src q)) (Name (Var q))
-> TermOf' q
-> InferOf q
inferBody [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
termBinds ContextOf' q
context [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx Subst (Origin (Src q)) (Name (Var q))
subst TermOf' q
expr = do
ContextOf' q
ctx1 <- [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall v loc.
IsVar v =>
[Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls ((Origin (Src q)
-> (Name (Var q), Type' (Src q) (Var q))
-> Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q)))
-> [Origin (Src q)]
-> [(Name (Var q), Type' (Src q) (Var q))]
-> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Origin (Src q)
loc (Name (Var q)
v, Type' (Src q) (Var q)
ty) -> Origin (Src q)
-> Name (Var q)
-> Type' (Src q) (Var q)
-> Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))
forall loc var a. loc -> var -> a -> Bind loc var a
Bind Origin (Src q)
loc Name (Var q)
v Type' (Src q) (Var q)
ty) [Origin (Src q)]
locBinds ([(Name (Var q), Type' (Src q) (Var q))]
-> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))])
-> [(Name (Var q), Type' (Src q) (Var q))]
-> [Bind (Origin (Src q)) (Name (Var q)) (Type' (Src q) (Var q))]
forall a b. (a -> b) -> a -> b
$ ((Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q)))
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> [(Name (Var q), Type' (Src q) (Var q))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q)))
-> (Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q), Type' (Src q) (Var q))
forall a b. (a -> b) -> a -> b
$ Signature (Origin (Src q)) (Name (Var q)) -> Type' (Src q) (Var q)
forall loc var. Signature loc var -> Type loc var
oldBvar (Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q))
-> (Signature (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst) [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
lhsCtx) (ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q))
-> ContextOf' q -> InferM (Src q) (Var q) (ContextOf' q)
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst ContextOf' q
context
(Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 TermOf' q
expr
let tyBinds :: [Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyBinds = (BindOf' q (TermOf' q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> [BindOf' q (TermOf' q)]
-> [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
-> [Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BindOf' q (TermOf' q)
bind TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhs -> BindOf' q (TermOf' q)
bind { bind'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bind'rhs = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
rhs }) [BindOf' q (TermOf' q)]
vs [TyTerm (Prim q) (Origin (Src q)) (Name (Var q))]
termBinds
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
subst Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
phi, Type' (Src q) (Var q)
-> Origin (Src q)
-> [Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> [Bind loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetRecE (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type' (Src q) (Var q)
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm) Origin (Src q)
topLoc [Bind
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyBinds TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
bodyTerm)
inferAssertType :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType :: ContextOf' q
-> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
inferAssertType ContextOf' q
ctx Origin (Src q)
loc TermOf' q
a TypeOf' q
ty = do
(Subst' (Src q) (Var q)
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
a
case Subst' (Src q) (Var q)
-> TypeOf' q
-> TypeOf' q
-> Either
(TypeError (Src q) (Name (Var q))) (Subst' (Src q) (Var q))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' (Src q) (Var q)
phi TypeOf' q
ty (TyTerm (Prim q) (Origin (Src q)) (Name (Var q)) -> TypeOf' q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm) of
Right Subst' (Src q) (Var q)
subst -> do
let subst' :: Subst' (Src q) (Var q)
subst' = Subst' (Src q) (Var q)
phi Subst' (Src q) (Var q)
-> Subst' (Src q) (Var q) -> Subst' (Src q) (Var q)
forall a. Semigroup a => a -> a -> a
<> Subst' (Src q) (Var q)
subst
(Subst' (Src q) (Var q),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst' (Src q) (Var q)
subst', Subst' (Src q) (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' (Src q) (Var q)
subst' (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TypeOf' q
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc prim v.
loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v
tyAssertTypeE Origin (Src q)
loc TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
aTyTerm TypeOf' q
ty)
Left TypeError (Src q) (Name (Var q))
err -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom TypeError (Src q) (Name (Var q))
err Origin (Src q)
loc
inferConstr :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr :: ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
inferConstr ContextOf' q
ctx Origin (Src q)
loc Name (Var q)
tag = do
case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx Name (Var q)
tag ContextOf' q
ctx of
Just Signature (Origin (Src q)) (Name (Var q))
ty -> do
Type (Origin (Src q)) (Name (Var q))
vT <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance Signature (Origin (Src q)) (Name (Var q))
ty
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Origin (Src q)
-> Type (Origin (Src q)) (Name (Var q))
-> Name (Var q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim. loc -> Type loc v -> v -> TyTerm prim loc v
tyConstrE Origin (Src q)
loc Type (Origin (Src q)) (Name (Var q))
vT Name (Var q)
tag)
Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc) Name (Var q)
tag) Origin (Src q)
loc
inferCase :: forall q . Lang q
=> ContextOf' q -> Origin (Src q) -> TermOf' q -> [CaseAltOf' q (TermOf' q)]
-> InferOf q
inferCase :: ContextOf' q
-> Origin (Src q)
-> TermOf' q
-> [CaseAltOf' q (TermOf' q)]
-> InferOf q
inferCase ContextOf' q
ctx Origin (Src q)
loc TermOf' q
e [CaseAltOf' q (TermOf' q)]
caseAlts = do
(Subst (Origin (Src q)) (Name (Var q))
phi, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
e
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
mAlts <- Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
inferAlts Subst (Origin (Src q)) (Name (Var q))
phi (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) ([CaseAltOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall a b. (a -> b) -> a -> b
$ [CaseAltOf' q (TermOf' q)]
caseAlts
case Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
mAlts of
Just (Subst (Origin (Src q)) (Name (Var q))
psi, Type (Origin (Src q)) (Name (Var q))
tRes, [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyAlts) -> (Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return ( Subst (Origin (Src q)) (Name (Var q))
psi
, Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
psi (TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim.
Type loc v
-> loc
-> TyTerm prim loc v
-> [CaseAlt loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
tyCaseE Type (Origin (Src q)) (Name (Var q))
tRes Origin (Src q)
loc (Subst (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
psi TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermE) [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
tyAlts)
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
Nothing -> TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
forall q.
Lang q =>
TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
retryWithBottom (Src q -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> TypeError loc var
EmptyCaseExpr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin Origin (Src q)
loc)) Origin (Src q)
loc
where
inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)]))
inferAlts :: Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> [CaseAltOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
inferAlts Subst (Origin (Src q)) (Name (Var q))
substE Type (Origin (Src q)) (Name (Var q))
tE [CaseAltOf' q (TermOf' q)]
alts = do
(Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
_, Maybe (Type (Origin (Src q)) (Name (Var q)))
mTRes, [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
as) <- ((Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
-> (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> [CaseAltOf' q (TermOf' q)]
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
go (Subst (Origin (Src q)) (Name (Var q))
substE, Type (Origin (Src q)) (Name (Var q))
tE, Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. Maybe a
Nothing, []) [CaseAltOf' q (TermOf' q)]
alts
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])))
-> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]))
forall a b. (a -> b) -> a -> b
$ case Maybe (Type (Origin (Src q)) (Name (Var q)))
mTRes of
Just Type (Origin (Src q)) (Name (Var q))
tRes -> (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall a. a -> Maybe a
Just (Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
tRes, [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. [a] -> [a]
L.reverse [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
as)
Maybe (Type (Origin (Src q)) (Name (Var q)))
Nothing -> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall a. Maybe a
Nothing
where
go :: (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> CaseAltOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
go initSt :: (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt@(Subst (Origin (Src q)) (Name (Var q))
subst, Type (Origin (Src q)) (Name (Var q))
tyTop, Maybe (Type (Origin (Src q)) (Name (Var q)))
mTyPrevRhs, [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res) CaseAltOf' q (TermOf' q)
alt = do
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
mRes <- CaseAltOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
inferAlt (Subst (Origin (Src q)) (Name (Var q))
-> CaseAltOf' q (TermOf' q) -> CaseAltOf' q (TermOf' q)
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst CaseAltOf' q (TermOf' q)
alt)
case Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
mRes of
Just (Subst (Origin (Src q)) (Name (Var q))
phi, Type (Origin (Src q)) (Name (Var q))
tyRhs, Type (Origin (Src q)) (Name (Var q))
tResExpected, CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1) -> do
let subst1 :: Subst (Origin (Src q)) (Name (Var q))
subst1 = Subst (Origin (Src q)) (Name (Var q))
subst Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
-> Subst (Origin (Src q)) (Name (Var q))
forall a. Semigroup a => a -> a -> a
<> Subst (Origin (Src q)) (Name (Var q))
phi
case Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
(TypeError (Src q) (Name (Var q)))
(Subst (Origin (Src q)) (Name (Var q)))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin (Src q)) (Name (Var q))
subst1 (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 Type (Origin (Src q)) (Name (Var q))
tyTop) (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst1 Type (Origin (Src q)) (Name (Var q))
tResExpected) of
Right Subst (Origin (Src q)) (Name (Var q))
subst2 -> do
case Maybe (Type (Origin (Src q)) (Name (Var q)))
mTyPrevRhs of
Maybe (Type (Origin (Src q)) (Name (Var q)))
Nothing -> (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q))
subst2, Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyTop, Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. a -> Maybe a
Just (Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q))))
-> Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyRhs, Subst (Origin (Src q)) (Name (Var q))
-> CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst2 CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1 CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. a -> [a] -> [a]
: [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res)
Just Type (Origin (Src q)) (Name (Var q))
tyPrevRhs -> do
case Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Either
(TypeError (Src q) (Name (Var q)))
(Subst (Origin (Src q)) (Name (Var q)))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin (Src q)) (Name (Var q))
subst2 (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyRhs) (Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst2 Type (Origin (Src q)) (Name (Var q))
tyPrevRhs) of
Right Subst (Origin (Src q)) (Name (Var q))
subst3 -> (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q))
subst3, Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst3 Type (Origin (Src q)) (Name (Var q))
tyTop, Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a. a -> Maybe a
Just (Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q))))
-> Type (Origin (Src q)) (Name (Var q))
-> Maybe (Type (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Subst (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin (Src q)) (Name (Var q))
subst3 Type (Origin (Src q)) (Name (Var q))
tyRhs, Subst (Origin (Src q)) (Name (Var q))
-> CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
forall (f :: * -> * -> *) v loc loc v.
(CanApply f, Ord v) =>
Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst (Origin (Src q)) (Name (Var q))
subst3 CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt1 CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
-> [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
forall a. a -> [a] -> [a]
: [CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))]
res)
Left TypeError (Src q) (Name (Var q))
err -> do
[TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt
Left TypeError (Src q) (Name (Var q))
err -> do
[TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TypeError (Src q) (Name (Var q))
err]
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
Nothing -> do
[TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Src q -> Name (Var q) -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin (Origin (Src q) -> Src q) -> Origin (Src q) -> Src q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Origin (Src q)
forall loc v a. CaseAlt loc v a -> loc
caseAlt'loc CaseAltOf' q (TermOf' q)
alt) (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt)]
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
-> InferM
(Src q)
(Var q)
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Maybe (Type (Origin (Src q)) (Name (Var q))),
[CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))])
initSt
inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q)))
inferAlt :: CaseAltOf' q (TermOf' q)
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
inferAlt CaseAltOf' q (TermOf' q)
alt =
case Name (Var q)
-> ContextOf' q
-> Maybe (Signature (Origin (Src q)) (Name (Var q)))
forall v loc.
Ord v =>
v -> Context loc v -> Maybe (Signature loc v)
lookupConstructorCtx (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt) ContextOf' q
ctx of
Just Signature (Origin (Src q)) (Name (Var q))
ctxConTy -> do
Type (Origin (Src q)) (Name (Var q))
conTy <- Signature (Origin (Src q)) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall v loc loc'.
IsVar v =>
Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance Signature (Origin (Src q)) (Name (Var q))
ctxConTy
let ([Type (Origin (Src q)) (Name (Var q))]
tyArgs, Type (Origin (Src q)) (Name (Var q))
tyRes) = Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
Type (Origin (Src q)) (Name (Var q)))
splitFunT Type (Origin (Src q)) (Name (Var q))
conTy
expectedArity :: Int
expectedArity = [Type (Origin (Src q)) (Name (Var q))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type (Origin (Src q)) (Name (Var q))]
tyArgs
actualArity :: Int
actualArity = [(Origin (Src q), Name (Var q))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Origin (Src q), Name (Var q))] -> Int)
-> [(Origin (Src q), Name (Var q))] -> Int
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> [(Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt
Bool -> InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
expectedArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
actualArity) (InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ())
-> InferM (Src q) (Var q) () -> InferM (Src q) (Var q) ()
forall a b. (a -> b) -> a -> b
$ [TypeError (Src q) (Name (Var q))] -> InferM (Src q) (Var q) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Src q
-> Name (Var q) -> Int -> Int -> TypeError (Src q) (Name (Var q))
forall loc var. loc -> var -> Int -> Int -> TypeError loc var
ConsArityMismatch (Origin (Src q) -> Src q
forall a. Origin a -> a
fromOrigin (Origin (Src q) -> Src q) -> Origin (Src q) -> Src q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> Origin (Src q)
forall loc v a. CaseAlt loc v a -> loc
caseAlt'loc CaseAltOf' q (TermOf' q)
alt) (CaseAltOf' q (TermOf' q) -> Name (Var q)
forall loc v a. CaseAlt loc v a -> v
caseAlt'tag CaseAltOf' q (TermOf' q)
alt) Int
expectedArity Int
actualArity]
let argVars :: [(Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars = (Type (Origin (Src q)) (Name (Var q))
-> (Origin (Src q), Name (Var q))
-> (Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q)))))
-> [Type (Origin (Src q)) (Name (Var q))]
-> [(Origin (Src q), Name (Var q))]
-> [(Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Type (Origin (Src q)) (Name (Var q))
ty (Origin (Src q)
src, Name (Var q)
arg) -> (Name (Var q)
arg, (Origin (Src q)
src, Type (Origin (Src q)) (Name (Var q))
ty))) [Type (Origin (Src q)) (Name (Var q))]
tyArgs (CaseAltOf' q (TermOf' q) -> [(Origin (Src q), Name (Var q))]
forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'args CaseAltOf' q (TermOf' q)
alt)
ctx1 :: ContextOf' q
ctx1 = Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
-> ContextOf' q
forall loc v.
Map v (Signature loc v) -> Map v (Signature loc v) -> Context loc v
Context ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q))))
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
-> Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ ((Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> [(Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
-> [(Name (Var q), Signature (Origin (Src q)) (Name (Var q)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q))))
-> ((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q)))
-> (Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))
-> (Name (Var q), Signature (Origin (Src q)) (Name (Var q)))
forall a b. (a -> b) -> a -> b
$ Type (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q))
forall loc src. Type loc src -> Signature loc src
monoT (Type (Origin (Src q)) (Name (Var q))
-> Signature (Origin (Src q)) (Name (Var q)))
-> ((Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q)))
-> (Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Signature (Origin (Src q)) (Name (Var q))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Origin (Src q), Type (Origin (Src q)) (Name (Var q)))
-> Type (Origin (Src q)) (Name (Var q))
forall a b. (a, b) -> b
snd) [(Name (Var q),
(Origin (Src q), Type (Origin (Src q)) (Name (Var q))))]
argVars) Map (Name (Var q)) (Signature (Origin (Src q)) (Name (Var q)))
forall a. Monoid a => a
mempty ContextOf' q -> ContextOf' q -> ContextOf' q
forall a. Semigroup a => a -> a -> a
<> ContextOf' q
ctx
(Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs) <- ContextOf' q -> TermOf' q -> InferOf q
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx1 (TermOf' q -> InferOf q) -> TermOf' q -> InferOf q
forall a b. (a -> b) -> a -> b
$ CaseAltOf' q (TermOf' q) -> TermOf' q
forall loc v a. CaseAlt loc v a -> a
caseAlt'rhs CaseAltOf' q (TermOf' q)
alt
let alt' :: CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt' = CaseAltOf' q (TermOf' q)
alt { caseAlt'rhs :: TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
caseAlt'rhs = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs }
Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))))
-> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall a b. (a -> b) -> a -> b
$ (Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
forall a. a -> Maybe a
Just (Subst (Origin (Src q)) (Name (Var q))
subst, TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
-> Type (Origin (Src q)) (Name (Var q))
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
tyTermRhs, Type (Origin (Src q)) (Name (Var q))
tyRes, CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
alt')
Maybe (Signature (Origin (Src q)) (Name (Var q)))
Nothing -> Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
-> InferM
(Src q)
(Var q)
(Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
(Subst (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
Type (Origin (Src q)) (Name (Var q)),
CaseAlt
(Origin (Src q))
(Name (Var q))
(TyTerm (Prim q) (Origin (Src q)) (Name (Var q))))
forall a. Maybe a
Nothing
splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)
splitFunT :: Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
Type (Origin (Src q)) (Name (Var q)))
splitFunT Type (Origin (Src q)) (Name (Var q))
arrT = [Type (Origin (Src q)) (Name (Var q))]
-> Type (Origin (Src q)) (Name (Var q))
-> ([Type (Origin (Src q)) (Name (Var q))],
Type (Origin (Src q)) (Name (Var q)))
forall loc var.
[Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go [] Type (Origin (Src q)) (Name (Var q))
arrT
where
go :: [Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go [Type loc var]
argsT (Type (Fix TypeF loc var (Fix (TypeF loc var))
t)) = case TypeF loc var (Fix (TypeF loc var))
t of
ArrowT loc
_loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b -> [Type loc var] -> Type loc var -> ([Type loc var], Type loc var)
go (Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF loc var)
a Type loc var -> [Type loc var] -> [Type loc var]
forall a. a -> [a] -> [a]
: [Type loc var]
argsT) (Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF loc var)
b)
TypeF loc var (Fix (TypeF loc var))
other -> ([Type loc var] -> [Type loc var]
forall a. [a] -> [a]
reverse [Type loc var]
argsT, Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF loc var) -> Type loc var)
-> Fix (TypeF loc var) -> Type loc var
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF loc var (Fix (TypeF loc var))
other)
applyAlt :: Subst loc v -> CaseAlt loc v (f loc v) -> CaseAlt loc v (f loc v)
applyAlt Subst loc v
subst CaseAlt loc v (f loc v)
alt = CaseAlt loc v (f loc v)
alt { caseAlt'rhs :: f loc v
caseAlt'rhs = Subst loc v -> f loc v -> f loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
subst (f loc v -> f loc v) -> f loc v -> f loc v
forall a b. (a -> b) -> a -> b
$ CaseAlt loc v (f loc v) -> f loc v
forall loc v a. CaseAlt loc v a -> a
caseAlt'rhs CaseAlt loc v (f loc v)
alt }
inferBottom :: Lang q => Origin (Src q) -> InferOf q
inferBottom :: Origin (Src q) -> InferOf q
inferBottom Origin (Src q)
loc = do
Type (Origin (Src q)) (Name (Var q))
ty <- (Name (Var q) -> Type (Origin (Src q)) (Name (Var q)))
-> InferM (Src q) (Var q) (Name (Var q))
-> InferM (Src q) (Var q) (Type (Origin (Src q)) (Name (Var q)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin (Src q)
-> Name (Var q) -> Type (Origin (Src q)) (Name (Var q))
forall loc var. loc -> var -> Type loc var
varT Origin (Src q)
loc) InferM (Src q) (Var q) (Name (Var q))
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
(Subst (Origin (Src q)) (Name (Var q)),
TyTerm (Prim q) (Origin (Src q)) (Name (Var q)))
-> InferOf q
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst (Origin (Src q)) (Name (Var q))
forall a. Monoid a => a
mempty, Type (Origin (Src q)) (Name (Var q))
-> Origin (Src q)
-> TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
forall loc v prim. Type loc v -> loc -> TyTerm prim loc v
tyBottomE Type (Origin (Src q)) (Name (Var q))
ty Origin (Src q)
loc)
newInstance :: IsVar v => Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance :: Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
newInstance = ((Subst loc (Name v), Type loc (Name v)) -> Type loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Type loc (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Subst loc (Name v) -> Type loc (Name v) -> Type loc (Name v))
-> (Subst loc (Name v), Type loc (Name v)) -> Type loc (Name v)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Subst loc (Name v) -> Type loc (Name v) -> Type loc (Name v)
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply) (InferM loc' v (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Type loc (Name v)))
-> (Signature loc (Name v)
-> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> Signature loc (Name v)
-> InferM loc' v (Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> Fix (SignatureF loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall loc loc.
SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
go (Fix (SignatureF loc (Name v))
-> InferM loc' v (Subst loc (Name v), Type loc (Name v)))
-> (Signature loc (Name v) -> Fix (SignatureF loc (Name v)))
-> Signature loc (Name v)
-> InferM loc' v (Subst loc (Name v), Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature loc (Name v) -> Fix (SignatureF loc (Name v))
forall loc var. Signature loc var -> Fix (SignatureF loc var)
unSignature
where
go :: SignatureF loc (Name v) (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
go = \case
MonoT Type loc (Name v)
ty -> (Subst loc (Name v), Type loc (Name v))
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst loc (Name v)
forall a. Monoid a => a
mempty, Type loc (Name v)
ty)
ForAllT loc
loc Name v
v (Subst Map (Name v) (Type loc (Name v))
m, Type loc (Name v)
ty) -> (Name v -> (Subst loc (Name v), Type loc (Name v)))
-> InferM loc v (Name v)
-> InferM loc v (Subst loc (Name v), Type loc (Name v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name v
nv -> (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v))
-> Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall a b. (a -> b) -> a -> b
$ Name v
-> Type loc (Name v)
-> Map (Name v) (Type loc (Name v))
-> Map (Name v) (Type loc (Name v))
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name v
v (loc -> Name v -> Type loc (Name v)
forall loc var. loc -> var -> Type loc var
varT loc
loc Name v
nv) Map (Name v) (Type loc (Name v))
m, Type loc (Name v)
ty)) InferM loc v (Name v)
forall v loc. IsVar v => InferM loc v (Name v)
freshVar
newVar :: loc -> v -> Signature loc v
newVar :: loc -> v -> Signature loc v
newVar loc
loc v
tvn = Type loc v -> Signature loc v
forall loc src. Type loc src -> Signature loc src
monoT (Type loc v -> Signature loc v) -> Type loc v -> Signature loc v
forall a b. (a -> b) -> a -> b
$ loc -> v -> Type loc v
forall loc var. loc -> var -> Type loc var
varT loc
loc v
tvn
freshVar :: IsVar v => InferM loc v (Name v)
freshVar :: InferM loc v (Name v)
freshVar = do
Int
n <- InferM loc v Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> InferM loc v ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> InferM loc v ()) -> Int -> InferM loc v ()
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
Name v -> InferM loc v (Name v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name v -> InferM loc v (Name v))
-> Name v -> InferM loc v (Name v)
forall a b. (a -> b) -> a -> b
$ Int -> Name v
forall v. Int -> Name v
FreshName Int
n
inferTerms :: Lang q
=> ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms :: ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms ContextOf' q
ctx [TermOf' q]
ts = case [TermOf' q]
ts of
[] -> (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)]))
-> (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall a b. (a -> b) -> a -> b
$ (SubstOf' q
forall a. Monoid a => a
mempty, [])
TermOf' q
a:[TermOf' q]
as -> do
(SubstOf' q
phi, TyTermOf' q
termA) <- ContextOf' q
-> TermOf' q -> InferM (Src q) (Var q) (SubstOf' q, TyTermOf' q)
forall q. Lang q => ContextOf' q -> TermOf' q -> InferOf q
infer ContextOf' q
ctx TermOf' q
a
let ta :: TypeOf' q
ta = TyTermOf' q -> TypeOf' q
forall prim loc v. TyTerm prim loc v -> Type loc v
termType TyTermOf' q
termA
(SubstOf' q
psi, [(TypeOf' q, TyTermOf' q)]
tas) <- ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall q.
Lang q =>
ContextOf' q
-> [TermOf' q]
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
inferTerms (SubstOf' q -> ContextOf' q -> ContextOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
phi ContextOf' q
ctx) [TermOf' q]
as
(SubstOf' q, [(TypeOf' q, TyTermOf' q)])
-> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
forall (m :: * -> *) a. Monad m => a -> m a
return ( SubstOf' q
phi SubstOf' q -> SubstOf' q -> SubstOf' q
forall a. Semigroup a => a -> a -> a
<> SubstOf' q
psi
, (SubstOf' q -> TypeOf' q -> TypeOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
psi TypeOf' q
ta, SubstOf' q -> TyTermOf' q -> TyTermOf' q
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply SubstOf' q
psi TyTermOf' q
termA) (TypeOf' q, TyTermOf' q)
-> [(TypeOf' q, TyTermOf' q)] -> [(TypeOf' q, TyTermOf' q)]
forall a. a -> [a] -> [a]
: [(TypeOf' q, TyTermOf' q)]
tas
)
unify :: (IsVar v, Show loc)
=> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify :: Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x)) (Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y)) =
case (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y) of
(VarT Origin loc
loc Name v
tvn, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
t) ->
let phiTvn :: Type' loc v
phiTvn = Subst' loc v -> Origin loc -> Name v -> Type' loc v
forall v loc.
IsVar v =>
Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar Subst' loc v
phi Origin loc
loc Name v
tvn
phiT :: Type' loc v
phiT = Subst' loc v -> Type' loc v -> Type' loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
t))
in if Type' loc v
phiTvn Type' loc v -> Type' loc v -> Bool
forall v loc. Eq v => Type loc v -> Type loc v -> Bool
`eqIgnoreLoc` Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
tvn
then Subst' loc v
-> Origin loc
-> Name v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc (m :: * -> *).
(IsVar v, MonadError (TypeError loc (Name v)) m) =>
Subst' loc v
-> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend Subst' loc v
phi Origin loc
loc Name v
tvn Type' loc v
phiT
else Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi Type' loc v
phiTvn Type' loc v
phiT
(TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a, VarT Origin loc
locB Name v
v) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
locB Name v
v) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a)
(ConT Origin loc
locA Name v
n [Fix (TypeF (Origin loc) (Name v))]
xs, ConT Origin loc
locB Name v
m [Fix (TypeF (Origin loc) (Name v))]
ys) ->
if Name v
n Name v -> Name v -> Bool
forall a. Eq a => a -> a -> Bool
== Name v
m
then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB
(ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a1 Fix (TypeF (Origin loc) (Name v))
a2, ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b1 Fix (TypeF (Origin loc) (Name v))
b2) -> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
a1, Fix (TypeF (Origin loc) (Name v))
a2]) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
b1, Fix (TypeF (Origin loc) (Name v))
b2])
(TupleT Origin loc
locA [Fix (TypeF (Origin loc) (Name v))]
xs, TupleT Origin loc
locB [Fix (TypeF (Origin loc) (Name v))]
ys) ->
if [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
ys
then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB
(ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a, ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
a) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
b)
(TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
b) -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc (Type' loc v -> Loc (Type' loc v))
-> Type' loc v -> Loc (Type' loc v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
a) (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc (Type' loc v -> Loc (Type' loc v))
-> Type' loc v -> Loc (Type' loc v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
b)
where
unifyErr :: Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
unifyErr Origin loc
locA Origin loc
locB = TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$
loc
-> Type loc (Name v) -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr (Origin loc -> Origin loc -> loc
forall a. Show a => Origin a -> Origin a -> a
chooseUserOrigin Origin loc
locA Origin loc
locB)
((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin (Type' loc v -> Type loc (Name v))
-> Type' loc v -> Type loc (Name v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x))
((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin (Type' loc v -> Type loc (Name v))
-> Type' loc v -> Type loc (Name v)
forall a b. (a -> b) -> a -> b
$ Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
-> Fix (TypeF (Origin loc) (Name v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y))
eqIgnoreLoc :: Eq v => Type loc v -> Type loc v -> Bool
eqIgnoreLoc :: Type loc v -> Type loc v -> Bool
eqIgnoreLoc = Type () v -> Type () v -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Type () v -> Type () v -> Bool)
-> (Type loc v -> Type () v) -> Type loc v -> Type loc v -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (loc -> ()) -> Type loc v -> Type () v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc (() -> loc -> ()
forall a b. a -> b -> a
const ())
applyVar :: IsVar v => Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar :: Subst' loc v -> Origin loc -> Name v -> Type' loc v
applyVar (Subst Map (Name v) (Type' loc v)
subst) Origin loc
loc Name v
v = Type' loc v -> Maybe (Type' loc v) -> Type' loc v
forall a. a -> Maybe a -> a
fromMaybe (Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
v) (Maybe (Type' loc v) -> Type' loc v)
-> Maybe (Type' loc v) -> Type' loc v
forall a b. (a -> b) -> a -> b
$ Name v -> Map (Name v) (Type' loc v) -> Maybe (Type' loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name v
v Map (Name v) (Type' loc v)
subst
extend
:: (IsVar v, MonadError (TypeError loc (Name v)) m)
=> Subst' loc v -> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend :: Subst' loc v
-> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
extend Subst' loc v
phi Origin loc
loc Name v
tvn Type' loc v
ty
| Origin loc -> Name v -> Type' loc v
forall loc var. loc -> var -> Type loc var
varT Origin loc
loc Name v
tvn Type' loc v -> Type' loc v -> Bool
forall v loc. Eq v => Type loc v -> Type loc v -> Bool
`eqIgnoreLoc` Type' loc v
ty = Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
phi
| Name v -> VarSet (Origin loc) (Name v) -> Bool
forall var src. Ord var => var -> VarSet src var -> Bool
memberVarSet Name v
tvn (Type' loc v -> VarSet (Origin loc) (Name v)
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type' loc v
ty) = TypeError loc (Name v) -> m (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError loc (Name v) -> m (Subst' loc v))
-> TypeError loc (Name v) -> m (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ loc -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr (Origin loc -> loc
forall a. Origin a -> a
fromOrigin Origin loc
loc) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
ty)
| Bool
otherwise = Subst' loc v -> m (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst' loc v -> m (Subst' loc v))
-> Subst' loc v -> m (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ Subst' loc v
phi Subst' loc v -> Subst' loc v -> Subst' loc v
forall a. Semigroup a => a -> a -> a
<> Name v -> Type' loc v -> Subst' loc v
forall v loc. v -> Type loc v -> Subst loc v
delta Name v
tvn Type' loc v
ty
unifyl :: (IsVar v, Show loc)
=> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl :: Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
unifyl Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
(Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ [Type' loc v] -> [Type' loc v] -> [(Type' loc v, Type' loc v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type' loc v]
as [Type' loc v]
bs
where
go :: (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) Either (TypeError loc (Name v)) (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either (TypeError loc (Name v)) (Subst' loc v)
eSubst
subtypeOf :: (IsVar v, Show loc, Eq loc)
=> Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
subtypeOf :: Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
subtypeOf Type loc v
a Type loc v
b =
Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ (TypeError loc (Name v) -> TypeError loc v)
-> (Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeError loc (Name v) -> TypeError loc v
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError loc (Name v) -> TypeError loc v)
-> (TypeError loc (Name v) -> TypeError loc (Name v))
-> TypeError loc (Name v)
-> TypeError loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError loc (Name v) -> TypeError loc (Name v)
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
forall v loc.
Ord v =>
Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v))
-> (Subst (Origin loc) (Name v) -> Subst loc (Name v))
-> Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) (Name v) -> Subst loc (Name v)
forall v loc. Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall a b. (a -> b) -> a -> b
$
Subst (Origin loc) (Name v)
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst (Origin loc) (Name v)
forall a. Monoid a => a
mempty ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
Proven Type loc v
a) ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode Type loc v
b)
genSubtypeOf :: (IsVar v, Show loc)
=> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf :: Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
phi tx :: Type' loc v
tx@(Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x)) ty :: Type' loc v
ty@(Type (Fix TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y)) = case (TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
x, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
y) of
(TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
_, VarT Origin loc
_ Name v
_) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst' loc v
phi Type' loc v
tx Type' loc v
ty
(ConT Origin loc
locA Name v
n [Fix (TypeF (Origin loc) (Name v))]
xs, ConT Origin loc
locB Name v
m [Fix (TypeF (Origin loc) (Name v))]
ys) ->
if Name v
n Name v -> Name v -> Bool
forall a. Eq a => a -> a -> Bool
== Name v
m
then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
xs) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
ys)
else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB
(ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a1 Fix (TypeF (Origin loc) (Name v))
a2, ArrowT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b1 Fix (TypeF (Origin loc) (Name v))
b2) -> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
a1, Fix (TypeF (Origin loc) (Name v))
a2]) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))
b1, Fix (TypeF (Origin loc) (Name v))
b2])
(TupleT Origin loc
locA [Fix (TypeF (Origin loc) (Name v))]
as, TupleT Origin loc
locB [Fix (TypeF (Origin loc) (Name v))]
bs) ->
if [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Fix (TypeF (Origin loc) (Name v))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fix (TypeF (Origin loc) (Name v))]
bs
then Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
phi ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
as) ((Fix (TypeF (Origin loc) (Name v)) -> Type' loc v)
-> [Fix (TypeF (Origin loc) (Name v))] -> [Type' loc v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type [Fix (TypeF (Origin loc) (Name v))]
bs)
else Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB
(ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
a, ListT Origin loc
_ Fix (TypeF (Origin loc) (Name v))
b) -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
phi (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
a) (Fix (TypeF (Origin loc) (Name v)) -> Type' loc v
forall loc var. Fix (TypeF loc var) -> Type loc var
Type Fix (TypeF (Origin loc) (Name v))
b)
(VarT Origin loc
locA Name v
_, TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v)))
_) -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
ty)
(TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v))),
TypeF (Origin loc) (Name v) (Fix (TypeF (Origin loc) (Name v))))
_ -> Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
tx) (Type' loc v -> Loc (Type' loc v)
forall f. HasLoc f => f -> Loc f
getLoc Type' loc v
ty)
where
subtypeErr :: Origin loc
-> Origin loc -> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeErr Origin loc
locA Origin loc
locB = TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
(TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> TypeError loc (Name v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ loc
-> Type loc (Name v) -> Type loc (Name v) -> TypeError loc (Name v)
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr (Origin loc -> Origin loc -> loc
forall a. Show a => Origin a -> Origin a -> a
chooseUserOrigin Origin loc
locA Origin loc
locB) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
tx) ((Origin loc -> loc) -> Type' loc v -> Type loc (Name v)
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin Type' loc v
ty)
subtypeOfL :: (IsVar v, Show loc)
=> Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL :: Subst' loc v
-> [Type' loc v]
-> [Type' loc v]
-> Either (TypeError loc (Name v)) (Subst' loc v)
subtypeOfL Subst' loc v
subst [Type' loc v]
as [Type' loc v]
bs = ((Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
(Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst' loc v
subst) ([(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v))
-> [(Type' loc v, Type' loc v)]
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall a b. (a -> b) -> a -> b
$ [Type' loc v] -> [Type' loc v] -> [(Type' loc v, Type' loc v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type' loc v]
as [Type' loc v]
bs
where
go :: (Type' loc v, Type' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
go (Type' loc v
a, Type' loc v
b) Either (TypeError loc (Name v)) (Subst' loc v)
eSubst = (\Subst' loc v
t -> Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
genSubtypeOf Subst' loc v
t Type' loc v
a Type' loc v
b) (Subst' loc v -> Either (TypeError loc (Name v)) (Subst' loc v))
-> Either (TypeError loc (Name v)) (Subst' loc v)
-> Either (TypeError loc (Name v)) (Subst' loc v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either (TypeError loc (Name v)) (Subst' loc v)
eSubst
addDecls :: IsVar v
=> [Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecls :: [Bind (Origin loc) (Name v) (Type' loc v)]
-> Context' loc v -> InferM loc v (Context' loc v)
addDecls [Bind (Origin loc) (Name v) (Type' loc v)]
vs Context' loc v
ctx =
(Context' loc v
-> Bind (Origin loc) (Name v) (Type' loc v)
-> InferM loc v (Context' loc v))
-> Context' loc v
-> [Bind (Origin loc) (Name v) (Type' loc v)]
-> InferM loc v (Context' loc v)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Context' loc v
c Bind (Origin loc) (Name v) (Type' loc v)
b -> VarSet' loc v
-> Bind (Origin loc) (Name v) (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
forall loc v.
IsVar v =>
VarSet' loc v
-> Bind' loc v (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecl VarSet' loc v
unknowns Bind (Origin loc) (Name v) (Type' loc v)
b Context' loc v
c) Context' loc v
ctx [Bind (Origin loc) (Name v) (Type' loc v)]
vs
where
unknowns :: VarSet' loc v
unknowns = (Signature (Origin loc) (Name v) -> VarSet' loc v)
-> Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Signature (Origin loc) (Name v) -> VarSet' loc v
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars (Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v)
-> Map (Name v) (Signature (Origin loc) (Name v)) -> VarSet' loc v
forall a b. (a -> b) -> a -> b
$ Context' loc v -> Map (Name v) (Signature (Origin loc) (Name v))
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds Context' loc v
ctx
addDecl :: forall loc v . IsVar v
=> VarSet' loc v
-> Bind' loc v (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecl :: VarSet' loc v
-> Bind' loc v (Type' loc v)
-> Context' loc v
-> InferM loc v (Context' loc v)
addDecl VarSet' loc v
unknowns Bind' loc v (Type' loc v)
b Context' loc v
ctx = do
Signature' loc v
scheme <- VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
toScheme VarSet' loc v
unknowns (Bind' loc v (Type' loc v) -> Type' loc v
forall loc var a. Bind loc var a -> a
bind'rhs Bind' loc v (Type' loc v)
b)
Context' loc v -> InferM loc v (Context' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Context' loc v -> InferM loc v (Context' loc v))
-> Context' loc v -> InferM loc v (Context' loc v)
forall a b. (a -> b) -> a -> b
$ Context' loc v
ctx
{ context'binds :: Map (Name v) (Signature' loc v)
context'binds = Name v
-> Signature' loc v
-> Map (Name v) (Signature' loc v)
-> Map (Name v) (Signature' loc v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Bind' loc v (Type' loc v) -> Name v
forall loc var a. Bind loc var a -> var
bind'lhs Bind' loc v (Type' loc v)
b) Signature' loc v
scheme (Map (Name v) (Signature' loc v)
-> Map (Name v) (Signature' loc v))
-> (Context' loc v -> Map (Name v) (Signature' loc v))
-> Context' loc v
-> Map (Name v) (Signature' loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' loc v -> Map (Name v) (Signature' loc v)
forall loc v. Context loc v -> Map v (Signature loc v)
context'binds (Context' loc v -> Map (Name v) (Signature' loc v))
-> Context' loc v -> Map (Name v) (Signature' loc v)
forall a b. (a -> b) -> a -> b
$ Context' loc v
ctx }
where
toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
toScheme VarSet' loc v
uVars Type' loc v
ty = do
(Subst (Origin loc) (Name v)
subst, [(Origin loc, Name v)]
newVars) <- ([((Origin loc, Name v), Name v)]
-> (Subst (Origin loc) (Name v), [(Origin loc, Name v)]))
-> InferM loc v [((Origin loc, Name v), Name v)]
-> InferM
loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[((Origin loc, Name v), Name v)]
xs -> ([((Origin loc, Name v), Name v)] -> Subst (Origin loc) (Name v)
forall loc. [((loc, Name v), Name v)] -> Subst loc (Name v)
toSubst [((Origin loc, Name v), Name v)]
xs, (((Origin loc, Name v), Name v) -> (Origin loc, Name v))
-> [((Origin loc, Name v), Name v)] -> [(Origin loc, Name v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((Origin loc
loc, Name v
_), Name v
v) -> (Origin loc
loc, Name v
v)) [((Origin loc, Name v), Name v)]
xs)) (InferM loc v [((Origin loc, Name v), Name v)]
-> InferM
loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)]))
-> InferM loc v [((Origin loc, Name v), Name v)]
-> InferM
loc v (Subst (Origin loc) (Name v), [(Origin loc, Name v)])
forall a b. (a -> b) -> a -> b
$
((Origin loc, Name v)
-> InferM loc v ((Origin loc, Name v), Name v))
-> [(Origin loc, Name v)]
-> InferM loc v [((Origin loc, Name v), Name v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Origin loc, Name v)
sv -> (Name v -> ((Origin loc, Name v), Name v))
-> InferM loc v (Name v)
-> InferM loc v ((Origin loc, Name v), Name v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Origin loc, Name v)
sv, )) InferM loc v (Name v)
forall v loc. IsVar v => InferM loc v (Name v)
freshVar) ([(Origin loc, Name v)]
-> InferM loc v [((Origin loc, Name v), Name v)])
-> [(Origin loc, Name v)]
-> InferM loc v [((Origin loc, Name v), Name v)]
forall a b. (a -> b) -> a -> b
$ VarSet' loc v -> [(Origin loc, Name v)]
forall src var. VarSet src var -> [(src, var)]
varSetToList VarSet' loc v
schematicVars
Signature' loc v -> InferM loc v (Signature' loc v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signature' loc v -> InferM loc v (Signature' loc v))
-> Signature' loc v -> InferM loc v (Signature' loc v)
forall a b. (a -> b) -> a -> b
$ ((Origin loc, Name v) -> Signature' loc v -> Signature' loc v)
-> Signature' loc v -> [(Origin loc, Name v)] -> Signature' loc v
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Origin loc -> Name v -> Signature' loc v -> Signature' loc v)
-> (Origin loc, Name v) -> Signature' loc v -> Signature' loc v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Origin loc -> Name v -> Signature' loc v -> Signature' loc v
forall loc v. loc -> v -> Signature loc v -> Signature loc v
forAllT) (Type' loc v -> Signature' loc v
forall loc src. Type loc src -> Signature loc src
monoT (Subst (Origin loc) (Name v) -> Type' loc v -> Type' loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst (Origin loc) (Name v)
subst Type' loc v
ty)) [(Origin loc, Name v)]
newVars
where
schematicVars :: VarSet' loc v
schematicVars = Type' loc v -> VarSet' loc v
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type' loc v
ty VarSet' loc v -> VarSet' loc v -> VarSet' loc v
forall var src.
Ord var =>
VarSet src var -> VarSet src var -> VarSet src var
`differenceVarSet` VarSet' loc v
uVars
toSubst :: [((loc, Name v), Name v)] -> Subst loc (Name v)
toSubst = Map (Name v) (Type loc (Name v)) -> Subst loc (Name v)
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map (Name v) (Type loc (Name v)) -> Subst loc (Name v))
-> ([((loc, Name v), Name v)] -> Map (Name v) (Type loc (Name v)))
-> [((loc, Name v), Name v)]
-> Subst loc (Name v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name v, Type loc (Name v))] -> Map (Name v) (Type loc (Name v))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name v, Type loc (Name v))] -> Map (Name v) (Type loc (Name v)))
-> ([((loc, Name v), Name v)] -> [(Name v, Type loc (Name v))])
-> [((loc, Name v), Name v)]
-> Map (Name v) (Type loc (Name v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((loc, Name v), Name v) -> (Name v, Type loc (Name v)))
-> [((loc, Name v), Name v)] -> [(Name v, Type loc (Name v))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((loc
loc, Name v
v), Name v
a) -> (Name v
v, loc -> Name v -> Type loc (Name v)
forall loc var. loc -> var -> Type loc var
varT loc
loc Name v
a))
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
unifyTypes :: (Show loc, IsVar v, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
unifyTypes :: Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
unifyTypes Type loc v
a Type loc v
b =
Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either (TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ (TypeError loc (Name v) -> TypeError loc v)
-> (Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeError loc (Name v) -> TypeError loc v
forall loc var. TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar (TypeError loc (Name v) -> TypeError loc v)
-> (TypeError loc (Name v) -> TypeError loc (Name v))
-> TypeError loc (Name v)
-> TypeError loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError loc (Name v) -> TypeError loc (Name v)
forall (m :: * -> * -> *) v loc.
(HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) =>
m loc (Name v) -> m loc (Name v)
normaliseType) (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
forall v loc.
Ord v =>
Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v))
-> (Subst (Origin loc) (Name v) -> Subst loc (Name v))
-> Subst (Origin loc) (Name v)
-> Either (TypeError loc v) (Subst loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) (Name v) -> Subst loc (Name v)
forall v loc. Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin) (Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v)))
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
-> Either
(TypeError loc v) (Either (TypeError loc v) (Subst loc v))
forall a b. (a -> b) -> a -> b
$
Subst (Origin loc) (Name v)
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst (Origin loc) (Name v))
forall v loc.
(IsVar v, Show loc) =>
Subst' loc v
-> Type' loc v
-> Type' loc v
-> Either (TypeError loc (Name v)) (Subst' loc v)
unify Subst (Origin loc) (Name v)
forall a. Monoid a => a
mempty ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
Proven Type loc v
a) ((v -> Name v) -> Type (Origin loc) v -> Type' loc v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Name v
forall v. v -> Name v
Name (Type (Origin loc) v -> Type' loc v)
-> Type (Origin loc) v -> Type' loc v
forall a b. (a -> b) -> a -> b
$ (loc -> Origin loc) -> Type loc v -> Type (Origin loc) v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc loc -> Origin loc
forall a. a -> Origin a
UserCode Type loc v
b)
fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var
fromTypeErrorNameVar = (TypeError loc var -> TypeError loc var)
-> (TypeError loc var -> TypeError loc var)
-> Either (TypeError loc var) (TypeError loc var)
-> TypeError loc var
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TypeError loc var -> TypeError loc var
forall a. a -> a
id TypeError loc var -> TypeError loc var
forall a. a -> a
id (Either (TypeError loc var) (TypeError loc var)
-> TypeError loc var)
-> (TypeError loc (Name var)
-> Either (TypeError loc var) (TypeError loc var))
-> TypeError loc (Name var)
-> TypeError loc var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
OccursErr loc
loc Type loc (Name var)
ty -> (Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc -> Type loc var -> TypeError loc var
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
ty)
UnifyErr loc
loc Type loc (Name var)
tA Type loc (Name var)
tB -> (Type loc var -> Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (loc -> Type loc var -> Type loc var -> TypeError loc var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tA) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tB)
SubtypeErr loc
loc Type loc (Name var)
tA Type loc (Name var)
tB -> (Type loc var -> Type loc var -> TypeError loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (Type loc var)
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (loc -> Type loc var -> Type loc var -> TypeError loc var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr loc
loc) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tA) (Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name var)
tB)
NotInScopeErr loc
loc Name var
v -> (var -> TypeError loc var)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (loc -> var -> TypeError loc var
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr loc
loc) (Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
EmptyCaseExpr loc
loc -> TypeError loc var -> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError loc var
-> Either (TypeError loc var) (TypeError loc var))
-> TypeError loc var
-> Either (TypeError loc var) (TypeError loc var)
forall a b. (a -> b) -> a -> b
$ loc -> TypeError loc var
forall loc var. loc -> TypeError loc var
EmptyCaseExpr loc
loc
ConsArityMismatch loc
loc Name var
v Int
expected Int
actual -> (var -> TypeError loc var)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
x -> loc -> var -> Int -> Int -> TypeError loc var
forall loc var. loc -> var -> Int -> Int -> TypeError loc var
ConsArityMismatch loc
loc var
x Int
expected Int
actual) (Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v)
TypeError loc (Name var)
FreshNameFound -> TypeError loc var -> Either (TypeError loc var) (TypeError loc var)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeError loc var
forall loc var. TypeError loc var
FreshNameFound
fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar (Type Fix (TypeF loc (Name var))
x) = (Fix (TypeF loc var) -> Type loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Type loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (TypeF loc var) -> Type loc var
forall loc var. Fix (TypeF loc var) -> Type loc var
Type (Either (TypeError loc var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Type loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Type loc var)
forall a b. (a -> b) -> a -> b
$ (TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc (Name var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall loc var.
TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
go Fix (TypeF loc (Name var))
x
where
go :: TypeF loc (Name var) (Fix (TypeF loc var)) -> Either (TypeError loc var) (Fix (TypeF loc var))
go :: TypeF loc (Name var) (Fix (TypeF loc var))
-> Either (TypeError loc var) (Fix (TypeF loc var))
go = \case
VarT loc
loc Name var
v -> (var -> Fix (TypeF loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> (var -> TypeF loc var (Fix (TypeF loc var)))
-> var
-> Fix (TypeF loc var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. loc -> var -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> var -> TypeF loc var r
VarT loc
loc) (Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
ConT loc
loc Name var
v [Fix (TypeF loc var)]
as -> (var -> Fix (TypeF loc var))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
con -> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc
-> var
-> [Fix (TypeF loc var)]
-> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> var -> [r] -> TypeF loc var r
ConT loc
loc var
con [Fix (TypeF loc var)]
as) (Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name var
v
ArrowT loc
loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (TypeF loc var)
-> Fix (TypeF loc var)
-> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> r -> r -> TypeF loc var r
ArrowT loc
loc Fix (TypeF loc var)
a Fix (TypeF loc var)
b
TupleT loc
loc [Fix (TypeF loc var)]
as -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc -> [Fix (TypeF loc var)] -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> [r] -> TypeF loc var r
TupleT loc
loc [Fix (TypeF loc var)]
as
ListT loc
loc Fix (TypeF loc var)
as -> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var)))
-> Fix (TypeF loc var)
-> Either (TypeError loc var) (Fix (TypeF loc var))
forall a b. (a -> b) -> a -> b
$ TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var))
-> TypeF loc var (Fix (TypeF loc var)) -> Fix (TypeF loc var)
forall a b. (a -> b) -> a -> b
$ loc -> Fix (TypeF loc var) -> TypeF loc var (Fix (TypeF loc var))
forall loc var r. loc -> r -> TypeF loc var r
ListT loc
loc Fix (TypeF loc var)
as
fromTyTermNameVar :: TyTerm prim loc (Name var) -> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar :: TyTerm prim loc (Name var)
-> Either (TypeError loc var) (TyTerm prim loc var)
fromTyTermNameVar (TyTerm Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
x) = (Fix (Ann (Type loc var) (TermF prim loc var))
-> TyTerm prim loc var)
-> Either
(TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either (TypeError loc var) (TyTerm prim loc var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix (Ann (Type loc var) (TermF prim loc var))
-> TyTerm prim loc var
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm (Either
(TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either (TypeError loc var) (TyTerm prim loc var))
-> Either
(TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either (TypeError loc var) (TyTerm prim loc var)
forall a b. (a -> b) -> a -> b
$ (Ann
(Type loc (Name var))
(TermF prim loc (Name var))
(Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either
(TypeError loc var)
(Fix (Ann (Type loc var) (TermF prim loc var))))
-> Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
-> Either
(TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
forall (m :: * -> *) (t :: * -> *) a.
(Monad m, Traversable t) =>
(t a -> m a) -> Fix t -> m a
foldFixM Ann
(Type loc (Name var))
(TermF prim loc (Name var))
(Fix (Ann (Type loc var) (TermF prim loc var)))
-> Either
(TypeError loc var) (Fix (Ann (Type loc var) (TermF prim loc var)))
forall t v prim.
Ann
(Type t (Name v))
(TermF prim t (Name v))
(Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
go Fix (Ann (Type loc (Name var)) (TermF prim loc (Name var)))
x
where
go :: Ann
(Type t (Name v))
(TermF prim t (Name v))
(Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
go (Ann Type t (Name v)
annTy TermF prim t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
term) = (Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v)))
-> Either (TypeError t v) (Type t v)
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\Type t v
t TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
val -> Ann
(Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
(Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v)))
-> Ann
(Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
forall a b. (a -> b) -> a -> b
$ Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Ann
(Type t v) (TermF prim t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann Type t v
t TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
val) (Type t (Name v) -> Either (TypeError t v) (Type t v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type t (Name v)
annTy) (Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Fix (Ann (Type t v) (TermF prim t v)))
forall a b. (a -> b) -> a -> b
$ case TermF prim t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
term of
Var t
loc Name v
v -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Var t
loc) (Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
Prim t
loc prim
p -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t -> prim -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> prim -> TermF prim loc v r
Prim t
loc prim
p
App t
loc Fix (Ann (Type t v) (TermF prim t v))
a Fix (Ann (Type t v) (TermF prim t v))
b -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t
-> Fix (Ann (Type t v) (TermF prim t v))
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> r -> r -> TermF prim loc v r
App t
loc Fix (Ann (Type t v) (TermF prim t v))
a Fix (Ann (Type t v) (TermF prim t v))
b
Lam t
loc Name v
v Fix (Ann (Type t v) (TermF prim t v))
a -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\v
arg -> t
-> v
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> r -> TermF prim loc v r
Lam t
loc v
arg Fix (Ann (Type t v) (TermF prim t v))
a) (Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v
Let t
loc Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
bind Fix (Ann (Type t v) (TermF prim t v))
a -> (Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
b -> t
-> Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> Bind loc v r -> r -> TermF prim loc v r
Let t
loc Bind t v (Fix (Ann (Type t v) (TermF prim t v)))
b Fix (Ann (Type t v) (TermF prim t v))
a) (Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
forall loc var a loc.
Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
bind
LetRec t
loc [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
binds Fix (Ann (Type t v) (TermF prim t v))
a -> ([Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
bs -> t
-> [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Fix (Ann (Type t v) (TermF prim t v))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r.
loc -> [Bind loc v r] -> r -> TermF prim loc v r
LetRec t
loc [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
bs Fix (Ann (Type t v) (TermF prim t v))
a) (Either
(TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
(TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ (Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v) [Bind t v (Fix (Ann (Type t v) (TermF prim t v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v) (Bind t v (Fix (Ann (Type t v) (TermF prim t v))))
forall loc var a loc.
Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind [Bind t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
binds
AssertType t
loc Fix (Ann (Type t v) (TermF prim t v))
a Type t (Name v)
ty -> (Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) (Type t v)
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
-> Fix (Ann (Type t v) (TermF prim t v))
-> Type t v
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> r -> Type loc v -> TermF prim loc v r
AssertType t
loc Fix (Ann (Type t v) (TermF prim t v))
a) (Either (TypeError t v) (Type t v)
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either (TypeError t v) (Type t v)
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ Type t (Name v) -> Either (TypeError t v) (Type t v)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type t (Name v)
ty
Constr t
loc Name v
v -> (v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either (TypeError t v) v
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> v -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Constr t
loc) (Name v -> Either (TypeError t v) v
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name v
v)
Bottom t
loc -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ t -> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r. loc -> TermF prim loc v r
Bottom t
loc
Case t
loc Fix (Ann (Type t v) (TermF prim t v))
e [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
alts -> ([CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
-> Either
(TypeError t v)
[CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
-> Fix (Ann (Type t v) (TermF prim t v))
-> [CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case t
loc Fix (Ann (Type t v) (TermF prim t v))
e) (Either
(TypeError t v)
[CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> Either
(TypeError t v)
[CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
(TermF prim t v (Fix (Ann (Type t v) (TermF prim t v))))
forall a b. (a -> b) -> a -> b
$ (CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))))
-> [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
-> Either
(TypeError t v)
[CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))
-> Either
(TypeError t v)
(CaseAlt t v (Fix (Ann (Type t v) (TermF prim t v))))
forall t t a loc.
CaseAlt t (Name t) a -> Either (TypeError loc t) (CaseAlt t t a)
fromAlt [CaseAlt t (Name v) (Fix (Ann (Type t v) (TermF prim t v)))]
alts
fromBind :: Bind loc (Name var) a
-> Either (TypeError loc var) (Bind loc var a)
fromBind Bind loc (Name var) a
b = (var -> Bind loc var a)
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\var
a -> Bind loc (Name var) a
b { bind'lhs :: var
bind'lhs = var
a }) (Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var a))
-> Either (TypeError loc var) var
-> Either (TypeError loc var) (Bind loc var a)
forall a b. (a -> b) -> a -> b
$ Name var -> Either (TypeError loc var) var
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar (Name var -> Either (TypeError loc var) var)
-> Name var -> Either (TypeError loc var) var
forall a b. (a -> b) -> a -> b
$ Bind loc (Name var) a -> Name var
forall loc var a. Bind loc var a -> var
bind'lhs Bind loc (Name var) a
b
fromAlt :: CaseAlt t (Name t) a -> Either (TypeError loc t) (CaseAlt t t a)
fromAlt alt :: CaseAlt t (Name t) a
alt@CaseAlt{a
t
[(t, Name t)]
Name t
caseAlt'rhs :: a
caseAlt'args :: [(t, Name t)]
caseAlt'tag :: Name t
caseAlt'loc :: t
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [(loc, v)]
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
..} =
(t -> [(t, t)] -> CaseAlt t t a)
-> Either (TypeError loc t) t
-> Either (TypeError loc t) [(t, t)]
-> Either (TypeError loc t) (CaseAlt t t a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\t
tag [(t, t)]
args -> CaseAlt t (Name t) a
alt { caseAlt'tag :: t
caseAlt'tag = t
tag, caseAlt'args :: [(t, t)]
caseAlt'args = [(t, t)]
args })
(Name t -> Either (TypeError loc t) t
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name t
caseAlt'tag)
(((t, Name t) -> Either (TypeError loc t) (t, t))
-> [(t, Name t)] -> Either (TypeError loc t) [(t, t)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (t, Name t) -> Either (TypeError loc t) (t, t)
forall t t loc. (t, Name t) -> Either (TypeError loc t) (t, t)
fromAltArg [(t, Name t)]
caseAlt'args)
fromAltArg :: (t, Name t) -> Either (TypeError loc t) (t, t)
fromAltArg (t
loc, Name t
v) = (t -> (t, t))
-> Either (TypeError loc t) t -> Either (TypeError loc t) (t, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t
loc , ) (Name t -> Either (TypeError loc t) t
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name t
v)
fromSubstNameVar :: Ord v => Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar :: Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
fromSubstNameVar (Subst Map (Name v) (Type loc (Name v))
m) = ([(v, Type loc v)] -> Subst loc v)
-> Either (TypeError loc v) [(v, Type loc v)]
-> Either (TypeError loc v) (Subst loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> ([(v, Type loc v)] -> Map v (Type loc v))
-> [(v, Type loc v)]
-> Subst loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(v, Type loc v)] -> Map v (Type loc v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList) (Either (TypeError loc v) [(v, Type loc v)]
-> Either (TypeError loc v) (Subst loc v))
-> Either (TypeError loc v) [(v, Type loc v)]
-> Either (TypeError loc v) (Subst loc v)
forall a b. (a -> b) -> a -> b
$ ((Name v, Type loc (Name v))
-> Either (TypeError loc v) (v, Type loc v))
-> [(Name v, Type loc (Name v))]
-> Either (TypeError loc v) [(v, Type loc v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name v, Type loc (Name v))
-> Either (TypeError loc v) (v, Type loc v)
forall a loc.
(Name a, Type loc (Name a))
-> Either (TypeError loc a) (a, Type loc a)
uncover ([(Name v, Type loc (Name v))]
-> Either (TypeError loc v) [(v, Type loc v)])
-> [(Name v, Type loc (Name v))]
-> Either (TypeError loc v) [(v, Type loc v)]
forall a b. (a -> b) -> a -> b
$ Map (Name v) (Type loc (Name v)) -> [(Name v, Type loc (Name v))]
forall k a. Map k a -> [(k, a)]
M.toList Map (Name v) (Type loc (Name v))
m
where
uncover :: (Name a, Type loc (Name a))
-> Either (TypeError loc a) (a, Type loc a)
uncover (Name a
v, Type loc (Name a)
ty) = (a -> Type loc a -> (a, Type loc a))
-> Either (TypeError loc a) a
-> Either (TypeError loc a) (Type loc a)
-> Either (TypeError loc a) (a, Type loc a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (Name a -> Either (TypeError loc a) a
forall v loc. Name v -> Either (TypeError loc v) v
fromNameVar Name a
v) (Type loc (Name a) -> Either (TypeError loc a) (Type loc a)
forall loc var.
Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
fromTypeNameVar Type loc (Name a)
ty)
fromSubstOrigin :: Ord v => Subst (Origin loc) v -> Subst loc v
fromSubstOrigin :: Subst (Origin loc) v -> Subst loc v
fromSubstOrigin = Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> (Subst (Origin loc) v -> Map v (Type loc v))
-> Subst (Origin loc) v
-> Subst loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type (Origin loc) v -> Type loc v)
-> Map v (Type (Origin loc) v) -> Map v (Type loc v)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Origin loc -> loc) -> Type (Origin loc) v -> Type loc v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc Origin loc -> loc
forall a. Origin a -> a
fromOrigin) (Map v (Type (Origin loc) v) -> Map v (Type loc v))
-> (Subst (Origin loc) v -> Map v (Type (Origin loc) v))
-> Subst (Origin loc) v
-> Map v (Type loc v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst (Origin loc) v -> Map v (Type (Origin loc) v)
forall loc v. Subst loc v -> Map v (Type loc v)
unSubst
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
printInfer :: (PrettyLang q) => (Either [ErrorOf q] (TypeOf q)) -> IO ()
printInfer :: Either [ErrorOf q] (TypeOf q) -> IO ()
printInfer = \case
Right TypeOf q
ty -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ TypeOf q -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty TypeOf q
ty
Left [ErrorOf q]
errs -> (ErrorOf q -> IO ()) -> [ErrorOf q] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> (ErrorOf q -> String) -> ErrorOf q -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") ShowS -> (ErrorOf q -> String) -> ErrorOf q -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (ErrorOf q -> Doc Any) -> ErrorOf q -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorOf q -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty) [ErrorOf q]
errs