{-# language MultiWayIf #-}
{-# language CPP #-}
{-# language AllowAmbiguousTypes #-}
{-# language ConstraintKinds #-}
{-# language ExistentialQuantification #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language RankNTypes #-}
{-# language TypeFamilies #-}
{-# options_ghc -Wno-name-shadowing #-}
module Nix.Type.Infer
( Constraint(..)
, TypeError(..)
, InferError(..)
, Subst(..)
, inferTop
)
where
import Nix.Prelude hiding ( Constraint
, Type
, TVar
)
import Control.Monad.Catch ( MonadThrow(..)
, MonadCatch(..)
)
import Control.Monad.Except ( MonadError(throwError,catchError) )
import Control.Monad.Logic
import Control.Monad.Fix ( MonadFix )
import Control.Monad.Ref ( MonadAtomicRef(..)
, MonadRef(..)
)
import Control.Monad.ST ( ST
, runST
)
import Data.Fix ( foldFix )
import qualified Data.HashMap.Lazy as M
import Data.List ( delete
, intersect
, (\\)
, (!!)
)
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe ( fromJust )
import qualified Data.Set as Set
import Nix.Atoms
import Nix.Convert
import Nix.Eval ( MonadEval(..) )
import qualified Nix.Eval as Eval
( eval
, evalWithAttrSet
)
import Nix.Expr.Types
import Nix.Fresh
import Nix.String
import Nix.Scope
import Nix.Type.Assumption hiding ( extend )
import qualified Nix.Type.Assumption as Assumption
import Nix.Type.Env
import qualified Nix.Type.Env as Env
import Nix.Type.Type
import Nix.Value.Monad
normalizeScheme :: Scheme -> Scheme
normalizeScheme :: Scheme -> Scheme
normalizeScheme (Forall [TVar]
_ Type
body) = [TVar] -> Type -> Scheme
Forall (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TVar, TVar)]
ord) (Type -> Type
normtype Type
body)
where
ord :: [(TVar, TVar)]
ord =
forall a b. [a] -> [b] -> [(a, b)]
zip
(forall a. Ord a => [a] -> [a]
ordNub forall a b. (a -> b) -> a -> b
$ forall {x}. (OneItem x ~ TVar, One x, Monoid x) => Type -> x
fv Type
body)
(Text -> TVar
TV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsString a => String -> a
fromString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
letters)
fv :: Type -> x
fv (TVar TVar
a ) = forall x. One x => OneItem x -> x
one TVar
a
fv (Type
a :~> Type
b ) = forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on forall a. Semigroup a => a -> a -> a
(<>) Type -> x
fv Type
a Type
b
fv (TCon Text
_ ) = forall a. Monoid a => a
mempty
fv (TSet Variadic
_ AttrSet Type
a) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> x
fv forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
M.elems AttrSet Type
a
fv (TList [Type]
a ) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> x
fv [Type]
a
fv (TMany [Type]
ts) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> x
fv [Type]
ts
normtype :: Type -> Type
normtype (Type
a :~> Type
b ) = Type -> Type
normtype Type
a Type -> Type -> Type
:~> Type -> Type
normtype Type
b
normtype (TCon Text
a ) = Text -> Type
TCon Text
a
normtype (TSet Variadic
b AttrSet Type
a) = Variadic -> AttrSet Type -> Type
TSet Variadic
b forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrSet Type
a
normtype (TList [Type]
a ) = [Type] -> Type
TList forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
a
normtype (TMany [Type]
ts) = [Type] -> Type
TMany forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts
normtype (TVar TVar
a ) =
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
(forall a t. (HasCallStack, IsText t) => t -> a
error Text
"type variable not in signature")
TVar -> Type
TVar
(forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup TVar
a [(TVar, TVar)]
ord)
generalize :: Set.Set TVar -> Type -> Scheme
generalize :: Set TVar -> Type -> Scheme
generalize Set TVar
free Type
t = [TVar] -> Type -> Scheme
Forall [TVar]
as Type
t
where
as :: [TVar]
as = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set TVar
free forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t
closeOver :: Type -> Scheme
closeOver :: Type -> Scheme
closeOver = Scheme -> Scheme
normalizeScheme forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVar -> Type -> Scheme
generalize forall a. Monoid a => a
mempty
allSameType :: [Type] -> Bool
allSameType :: [Type] -> Bool
allSameType = forall a. Eq a => [a] -> Bool
allSame
where
allSame :: Eq a => [a] -> Bool
allSame :: forall a. Eq a => [a] -> Bool
allSame [] = Bool
True
allSame (a
x:[a]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
x forall a. Eq a => a -> a -> Bool
==) [a]
xs
data TypeError
= UnificationFail Type Type
| InfiniteType TVar Type
| UnboundVariables [VarName]
| Ambigious [Constraint]
| UnificationMismatch [Type] [Type]
deriving (TypeError -> TypeError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeError -> TypeError -> Bool
$c/= :: TypeError -> TypeError -> Bool
== :: TypeError -> TypeError -> Bool
$c== :: TypeError -> TypeError -> Bool
Eq, Int -> TypeError -> ShowS
[TypeError] -> ShowS
TypeError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeError] -> ShowS
$cshowList :: [TypeError] -> ShowS
show :: TypeError -> String
$cshow :: TypeError -> String
showsPrec :: Int -> TypeError -> ShowS
$cshowsPrec :: Int -> TypeError -> ShowS
Show, Eq TypeError
TypeError -> TypeError -> Bool
TypeError -> TypeError -> Ordering
TypeError -> TypeError -> TypeError
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
min :: TypeError -> TypeError -> TypeError
$cmin :: TypeError -> TypeError -> TypeError
max :: TypeError -> TypeError -> TypeError
$cmax :: TypeError -> TypeError -> TypeError
>= :: TypeError -> TypeError -> Bool
$c>= :: TypeError -> TypeError -> Bool
> :: TypeError -> TypeError -> Bool
$c> :: TypeError -> TypeError -> Bool
<= :: TypeError -> TypeError -> Bool
$c<= :: TypeError -> TypeError -> Bool
< :: TypeError -> TypeError -> Bool
$c< :: TypeError -> TypeError -> Bool
compare :: TypeError -> TypeError -> Ordering
$ccompare :: TypeError -> TypeError -> Ordering
Ord)
data InferError
= TypeInferenceErrors [TypeError]
| TypeInferenceAborted
| forall s. Exception s => EvaluationError s
typeError :: MonadError InferError m => TypeError -> m ()
typeError :: forall (m :: * -> *). MonadError InferError m => TypeError -> m ()
typeError TypeError
err = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [TypeError] -> InferError
TypeInferenceErrors forall a b. (a -> b) -> a -> b
$ forall x. One x => OneItem x -> x
one TypeError
err
deriving instance Show InferError
instance Exception InferError
instance Semigroup InferError where
<> :: InferError -> InferError -> InferError
(<>) = forall a b. a -> b -> a
const
instance Monoid InferError where
mempty :: InferError
mempty = InferError
TypeInferenceAborted
newtype InferState = InferState Int
deriving
(InferState -> InferState -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InferState -> InferState -> Bool
$c/= :: InferState -> InferState -> Bool
== :: InferState -> InferState -> Bool
$c== :: InferState -> InferState -> Bool
Eq, Integer -> InferState
InferState -> InferState
InferState -> InferState -> InferState
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> InferState
$cfromInteger :: Integer -> InferState
signum :: InferState -> InferState
$csignum :: InferState -> InferState
abs :: InferState -> InferState
$cabs :: InferState -> InferState
negate :: InferState -> InferState
$cnegate :: InferState -> InferState
* :: InferState -> InferState -> InferState
$c* :: InferState -> InferState -> InferState
- :: InferState -> InferState -> InferState
$c- :: InferState -> InferState -> InferState
+ :: InferState -> InferState -> InferState
$c+ :: InferState -> InferState -> InferState
Num, Int -> InferState
InferState -> Int
InferState -> [InferState]
InferState -> InferState
InferState -> InferState -> [InferState]
InferState -> InferState -> InferState -> [InferState]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: InferState -> InferState -> InferState -> [InferState]
$cenumFromThenTo :: InferState -> InferState -> InferState -> [InferState]
enumFromTo :: InferState -> InferState -> [InferState]
$cenumFromTo :: InferState -> InferState -> [InferState]
enumFromThen :: InferState -> InferState -> [InferState]
$cenumFromThen :: InferState -> InferState -> [InferState]
enumFrom :: InferState -> [InferState]
$cenumFrom :: InferState -> [InferState]
fromEnum :: InferState -> Int
$cfromEnum :: InferState -> Int
toEnum :: Int -> InferState
$ctoEnum :: Int -> InferState
pred :: InferState -> InferState
$cpred :: InferState -> InferState
succ :: InferState -> InferState
$csucc :: InferState -> InferState
Enum, Eq InferState
InferState -> InferState -> Bool
InferState -> InferState -> Ordering
InferState -> InferState -> InferState
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
min :: InferState -> InferState -> InferState
$cmin :: InferState -> InferState -> InferState
max :: InferState -> InferState -> InferState
$cmax :: InferState -> InferState -> InferState
>= :: InferState -> InferState -> Bool
$c>= :: InferState -> InferState -> Bool
> :: InferState -> InferState -> Bool
$c> :: InferState -> InferState -> Bool
<= :: InferState -> InferState -> Bool
$c<= :: InferState -> InferState -> Bool
< :: InferState -> InferState -> Bool
$c< :: InferState -> InferState -> Bool
compare :: InferState -> InferState -> Ordering
$ccompare :: InferState -> InferState -> Ordering
Ord)
instance Semigroup InferState where
<> :: InferState -> InferState -> InferState
(<>) = forall a. Num a => a -> a -> a
(+)
instance Monoid InferState where
mempty :: InferState
mempty = InferState
0
initInfer :: InferState
initInfer :: InferState
initInfer = Int -> InferState
InferState Int
0
letters :: [String]
letters :: [String]
letters =
do
Int
l <- [Int
1 ..]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM
Int
l
[Char
'a' .. Char
'z']
freshTVar :: MonadState InferState m => m TVar
freshTVar :: forall (m :: * -> *). MonadState InferState m => m TVar
freshTVar =
do
InferState
s <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ InferState
s
pure $ Text -> TVar
TV forall a b. (a -> b) -> a -> b
$ forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ [String]
letters forall a. [a] -> Int -> a
!! coerce :: forall a b. Coercible a b => a -> b
coerce InferState
s
fresh :: MonadState InferState m => m Type
fresh :: forall (m :: * -> *). MonadState InferState m => m Type
fresh = TVar -> Type
TVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState InferState m => m TVar
freshTVar
intoFresh :: (Traversable t, MonadState InferState f) => t a -> f (t Type)
intoFresh :: forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, MonadState InferState f) =>
t a -> f (t Type)
intoFresh =
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b. a -> b -> a
const forall (m :: * -> *). MonadState InferState m => m Type
fresh)
instantiate :: MonadState InferState m => Scheme -> m Type
instantiate :: forall (m :: * -> *). MonadState InferState m => Scheme -> m Type
instantiate (Forall [TVar]
as Type
t) =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. Substitutable a => Subst -> a -> a
`apply` Type
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as) (forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, MonadState InferState f) =>
t a -> f (t Type)
intoFresh [TVar]
as)
data Constraint
= EqConst Type Type
| ExpInstConst Type Scheme
| ImpInstConst Type (Set.Set TVar) Type
deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show, Constraint -> Constraint -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constraint -> Constraint -> Bool
$c/= :: Constraint -> Constraint -> Bool
== :: Constraint -> Constraint -> Bool
$c== :: Constraint -> Constraint -> Bool
Eq, Eq Constraint
Constraint -> Constraint -> Bool
Constraint -> Constraint -> Ordering
Constraint -> Constraint -> Constraint
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
min :: Constraint -> Constraint -> Constraint
$cmin :: Constraint -> Constraint -> Constraint
max :: Constraint -> Constraint -> Constraint
$cmax :: Constraint -> Constraint -> Constraint
>= :: Constraint -> Constraint -> Bool
$c>= :: Constraint -> Constraint -> Bool
> :: Constraint -> Constraint -> Bool
$c> :: Constraint -> Constraint -> Bool
<= :: Constraint -> Constraint -> Bool
$c<= :: Constraint -> Constraint -> Bool
< :: Constraint -> Constraint -> Bool
$c< :: Constraint -> Constraint -> Bool
compare :: Constraint -> Constraint -> Ordering
$ccompare :: Constraint -> Constraint -> Ordering
Ord)
newtype Subst = Subst (Map TVar Type)
deriving (Subst -> Subst -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c== :: Subst -> Subst -> Bool
Eq, Eq Subst
Subst -> Subst -> Bool
Subst -> Subst -> Ordering
Subst -> Subst -> Subst
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
min :: Subst -> Subst -> Subst
$cmin :: Subst -> Subst -> Subst
max :: Subst -> Subst -> Subst
$cmax :: Subst -> Subst -> Subst
>= :: Subst -> Subst -> Bool
$c>= :: Subst -> Subst -> Bool
> :: Subst -> Subst -> Bool
$c> :: Subst -> Subst -> Bool
<= :: Subst -> Subst -> Bool
$c<= :: Subst -> Subst -> Bool
< :: Subst -> Subst -> Bool
$c< :: Subst -> Subst -> Bool
compare :: Subst -> Subst -> Ordering
$ccompare :: Subst -> Subst -> Ordering
Ord, Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Subst] -> ShowS
$cshowList :: [Subst] -> ShowS
show :: Subst -> String
$cshow :: Subst -> String
showsPrec :: Int -> Subst -> ShowS
$cshowsPrec :: Int -> Subst -> ShowS
Show, NonEmpty Subst -> Subst
Subst -> Subst -> Subst
forall b. Integral b => b -> Subst -> Subst
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Subst -> Subst
$cstimes :: forall b. Integral b => b -> Subst -> Subst
sconcat :: NonEmpty Subst -> Subst
$csconcat :: NonEmpty Subst -> Subst
<> :: Subst -> Subst -> Subst
$c<> :: Subst -> Subst -> Subst
Semigroup, Semigroup Subst
Subst
[Subst] -> Subst
Subst -> Subst -> Subst
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Subst] -> Subst
$cmconcat :: [Subst] -> Subst
mappend :: Subst -> Subst -> Subst
$cmappend :: Subst -> Subst -> Subst
mempty :: Subst
$cmempty :: Subst
Monoid)
compose :: Subst -> Subst -> Subst
compose :: Subst -> Subst -> Subst
compose a :: Subst
a@(Subst Map TVar Type
s2) (Subst Map TVar Type
s1) =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$
forall a. Substitutable a => Subst -> a -> a
apply Subst
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Map TVar Type
s2 forall a. Semigroup a => a -> a -> a
<> Map TVar Type
s1)
class Substitutable a where
apply :: Subst -> a -> a
instance Substitutable TVar where
apply :: Subst -> TVar -> TVar
apply (Subst Map TVar Type
s) TVar
a = TVar
tv
where
(TVar TVar
tv) = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (TVar -> Type
TVar TVar
a) TVar
a Map TVar Type
s
instance Substitutable Type where
apply :: Subst -> Type -> Type
apply Subst
_ ( TCon Text
a ) = Text -> Type
TCon Text
a
apply Subst
s ( TSet Variadic
b AttrSet Type
a ) = Variadic -> AttrSet Type -> Type
TSet Variadic
b forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrSet Type
a
apply Subst
s ( TList [Type]
a ) = [Type] -> Type
TList forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
a
apply (Subst Map TVar Type
s) t :: Type
t@(TVar TVar
a ) = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Type
t TVar
a Map TVar Type
s
apply Subst
s ( Type
t1 :~> Type
t2) = (Type -> Type -> Type
(:~>) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Substitutable a => Subst -> a -> a
apply Subst
s) Type
t1 Type
t2
apply Subst
s ( TMany [Type]
ts ) = [Type] -> Type
TMany forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts
instance Substitutable Scheme where
apply :: Subst -> Scheme -> Scheme
apply (Subst Map TVar Type
s) (Forall [TVar]
as Type
t) = [TVar] -> Type -> Scheme
Forall [TVar]
as forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
s' Type
t
where
s' :: Subst
s' = Map TVar Type -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map TVar Type
s [TVar]
as
instance Substitutable Constraint where
apply :: Subst -> Constraint -> Constraint
apply Subst
s (EqConst Type
t1 Type
t2) = forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Type -> Type -> Constraint
EqConst (forall a. Substitutable a => Subst -> a -> a
apply Subst
s) Type
t1 Type
t2
apply Subst
s (ExpInstConst Type
t Scheme
sc) =
Type -> Scheme -> Constraint
ExpInstConst
(forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t)
(forall a. Substitutable a => Subst -> a -> a
apply Subst
s Scheme
sc)
apply Subst
s (ImpInstConst Type
t1 Set TVar
ms Type
t2) =
Type -> Set TVar -> Type -> Constraint
ImpInstConst
(forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t1)
(forall a. Substitutable a => Subst -> a -> a
apply Subst
s Set TVar
ms)
(forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t2)
instance Substitutable a => Substitutable [a] where
apply :: Subst -> [a] -> [a]
apply = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => Subst -> a -> a
apply
instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
apply :: Subst -> Set a -> Set a
apply = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => Subst -> a -> a
apply
data Judgment s =
Judgment
{ forall s. Judgment s -> Assumption
assumptions :: Assumption
, forall s. Judgment s -> [Constraint]
typeConstraints :: [Constraint]
, forall s. Judgment s -> Type
inferredType :: Type
}
deriving Int -> Judgment s -> ShowS
forall s. Int -> Judgment s -> ShowS
forall s. [Judgment s] -> ShowS
forall s. Judgment s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Judgment s] -> ShowS
$cshowList :: forall s. [Judgment s] -> ShowS
show :: Judgment s -> String
$cshow :: forall s. Judgment s -> String
showsPrec :: Int -> Judgment s -> ShowS
$cshowsPrec :: forall s. Int -> Judgment s -> ShowS
Show
inferred :: Type -> Judgment s
inferred :: forall s. Type -> Judgment s
inferred = forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
type InferTInternals s m a =
ReaderT
(Set.Set TVar, Scopes (InferT s m) (Judgment s))
(StateT InferState (ExceptT InferError m))
a
newtype InferT s m a =
InferT
{ forall s (m :: * -> *) a. InferT s m a -> InferTInternals s m a
getInfer ::
InferTInternals s m a
}
deriving
( forall a b. a -> InferT s m b -> InferT s m a
forall a b. (a -> b) -> InferT s m a -> InferT s m b
forall s (m :: * -> *) a b.
Functor m =>
a -> InferT s m b -> InferT s m a
forall s (m :: * -> *) a b.
Functor m =>
(a -> b) -> InferT s m a -> InferT s m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> InferT s m b -> InferT s m a
$c<$ :: forall s (m :: * -> *) a b.
Functor m =>
a -> InferT s m b -> InferT s m a
fmap :: forall a b. (a -> b) -> InferT s m a -> InferT s m b
$cfmap :: forall s (m :: * -> *) a b.
Functor m =>
(a -> b) -> InferT s m a -> InferT s m b
Functor
, forall a. a -> InferT s m a
forall a b. InferT s m a -> InferT s m b -> InferT s m a
forall a b. InferT s m a -> InferT s m b -> InferT s m b
forall a b. InferT s m (a -> b) -> InferT s m a -> InferT s m b
forall a b c.
(a -> b -> c) -> InferT s m a -> InferT s m b -> InferT s m c
forall {s} {m :: * -> *}. Monad m => Functor (InferT s m)
forall s (m :: * -> *) a. Monad m => a -> InferT s m a
forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m a
forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m b
forall s (m :: * -> *) a b.
Monad m =>
InferT s m (a -> b) -> InferT s m a -> InferT s m b
forall s (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> InferT s m a -> InferT s m b -> InferT s m 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
<* :: forall a b. InferT s m a -> InferT s m b -> InferT s m a
$c<* :: forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m a
*> :: forall a b. InferT s m a -> InferT s m b -> InferT s m b
$c*> :: forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m b
liftA2 :: forall a b c.
(a -> b -> c) -> InferT s m a -> InferT s m b -> InferT s m c
$cliftA2 :: forall s (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> InferT s m a -> InferT s m b -> InferT s m c
<*> :: forall a b. InferT s m (a -> b) -> InferT s m a -> InferT s m b
$c<*> :: forall s (m :: * -> *) a b.
Monad m =>
InferT s m (a -> b) -> InferT s m a -> InferT s m b
pure :: forall a. a -> InferT s m a
$cpure :: forall s (m :: * -> *) a. Monad m => a -> InferT s m a
Applicative
, forall a. InferT s m a
forall a. InferT s m a -> InferT s m [a]
forall a. InferT s m a -> InferT s m a -> InferT s m a
forall s (m :: * -> *). Monad m => Applicative (InferT s m)
forall s (m :: * -> *) a. Monad m => InferT s m a
forall s (m :: * -> *) a. Monad m => InferT s m a -> InferT s m [a]
forall s (m :: * -> *) a.
Monad m =>
InferT s m a -> InferT s m a -> InferT s m a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
many :: forall a. InferT s m a -> InferT s m [a]
$cmany :: forall s (m :: * -> *) a. Monad m => InferT s m a -> InferT s m [a]
some :: forall a. InferT s m a -> InferT s m [a]
$csome :: forall s (m :: * -> *) a. Monad m => InferT s m a -> InferT s m [a]
<|> :: forall a. InferT s m a -> InferT s m a -> InferT s m a
$c<|> :: forall s (m :: * -> *) a.
Monad m =>
InferT s m a -> InferT s m a -> InferT s m a
empty :: forall a. InferT s m a
$cempty :: forall s (m :: * -> *) a. Monad m => InferT s m a
Alternative
, forall a. a -> InferT s m a
forall a b. InferT s m a -> InferT s m b -> InferT s m b
forall a b. InferT s m a -> (a -> InferT s m b) -> InferT s m b
forall s (m :: * -> *). Monad m => Applicative (InferT s m)
forall s (m :: * -> *) a. Monad m => a -> InferT s m a
forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m b
forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> (a -> InferT s m b) -> InferT s m 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 :: forall a. a -> InferT s m a
$creturn :: forall s (m :: * -> *) a. Monad m => a -> InferT s m a
>> :: forall a b. InferT s m a -> InferT s m b -> InferT s m b
$c>> :: forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> InferT s m b -> InferT s m b
>>= :: forall a b. InferT s m a -> (a -> InferT s m b) -> InferT s m b
$c>>= :: forall s (m :: * -> *) a b.
Monad m =>
InferT s m a -> (a -> InferT s m b) -> InferT s m b
Monad
, forall a. InferT s m a
forall a. InferT s m a -> InferT s m a -> InferT s m a
forall s (m :: * -> *). Monad m => Monad (InferT s m)
forall s (m :: * -> *). Monad m => Alternative (InferT s m)
forall s (m :: * -> *) a. Monad m => InferT s m a
forall s (m :: * -> *) a.
Monad m =>
InferT s m a -> InferT s m a -> InferT s m a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
mplus :: forall a. InferT s m a -> InferT s m a -> InferT s m a
$cmplus :: forall s (m :: * -> *) a.
Monad m =>
InferT s m a -> InferT s m a -> InferT s m a
mzero :: forall a. InferT s m a
$cmzero :: forall s (m :: * -> *) a. Monad m => InferT s m a
MonadPlus
, forall a. (a -> InferT s m a) -> InferT s m a
forall {s} {m :: * -> *}. MonadFix m => Monad (InferT s m)
forall s (m :: * -> *) a.
MonadFix m =>
(a -> InferT s m a) -> InferT s m a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
mfix :: forall a. (a -> InferT s m a) -> InferT s m a
$cmfix :: forall s (m :: * -> *) a.
MonadFix m =>
(a -> InferT s m a) -> InferT s m a
MonadFix
, MonadReader (Set.Set TVar, Scopes (InferT s m) (Judgment s))
, forall a. String -> InferT s m a
forall {s} {m :: * -> *}. MonadFail m => Monad (InferT s m)
forall s (m :: * -> *) a. MonadFail m => String -> InferT s m a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: forall a. String -> InferT s m a
$cfail :: forall s (m :: * -> *) a. MonadFail m => String -> InferT s m a
MonadFail
, MonadState InferState
, MonadError InferError
)
extendMSet :: forall s m a . Monad m => TVar -> InferT s m a -> InferT s m a
extendMSet :: forall s (m :: * -> *) a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet TVar
x = coerce :: forall a b. Coercible a b => a -> b
coerce InferTInternals s m a -> InferTInternals s m a
putSetElementM
where
putSetElementM :: InferTInternals s m a -> InferTInternals s m a
putSetElementM :: InferTInternals s m a -> InferTInternals s m a
putSetElementM = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> Set a -> Set a
Set.insert forall a b. (a -> b) -> a -> b
$ TVar
x)
instance MonadTrans (InferT s) where
lift :: forall (m :: * -> *) a. Monad m => m a -> InferT s m a
lift = forall s (m :: * -> *) a. InferTInternals s m a -> InferT s m a
InferT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
instance MonadRef m => MonadRef (InferT s m) where
type Ref (InferT s m) = Ref m
newRef :: forall a. a -> InferT s m (Ref (InferT s m) a)
newRef a
x = forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newRef a
x
readRef :: forall a. Ref (InferT s m) a -> InferT s m a
readRef Ref (InferT s m) a
x = forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readRef Ref (InferT s m) a
x
writeRef :: forall a. Ref (InferT s m) a -> a -> InferT s m ()
writeRef Ref (InferT s m) a
x a
y = forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeRef Ref (InferT s m) a
x a
y
instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
atomicModifyRef :: forall a b. Ref (InferT s m) a -> (a -> (a, b)) -> InferT s m b
atomicModifyRef Ref (InferT s m) a
x a -> (a, b)
f =
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer forall a b. (a -> b) -> a -> b
$
do
b
res <- forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (a, b)
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readRef Ref (InferT s m) a
x
()
_ <- forall (m :: * -> *) a. MonadRef m => Ref m a -> (a -> a) -> m ()
modifyRef Ref (InferT s m) a
x forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (a, b)
f
pure b
res
instance Monad m => MonadThrow (InferT s m) where
throwM :: forall e a. Exception e => e -> InferT s m a
throwM = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Exception s => s -> InferError
EvaluationError
instance Monad m => MonadCatch (InferT s m) where
catch :: forall e a.
Exception e =>
InferT s m a -> (e -> InferT s m a) -> InferT s m a
catch InferT s m a
m e -> InferT s m a
h =
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError InferT s m a
m forall a b. (a -> b) -> a -> b
$
\case
EvaluationError s
e ->
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
(forall a t. (HasCallStack, IsText t) => t -> a
error forall a b. (a -> b) -> a -> b
$ Text
"Exception was not an exception: " forall a. Semigroup a => a -> a -> a
<> forall b a. (Show a, IsString b) => a -> b
show s
e)
e -> InferT s m a
h
(forall e. Exception e => SomeException -> Maybe e
fromException forall a b. (a -> b) -> a -> b
$ forall e. Exception e => e -> SomeException
toException s
e)
InferError
err -> forall a t. (HasCallStack, IsText t) => t -> a
error forall a b. (a -> b) -> a -> b
$ Text
"Unexpected error: " forall a. Semigroup a => a -> a -> a
<> forall b a. (Show a, IsString b) => a -> b
show InferError
err
instance
Monad m
=> FromValue NixString (InferT s m) (Judgment s)
where
fromValueMay :: Judgment s -> InferT s m (Maybe NixString)
fromValueMay Judgment s
_ = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
fromValue :: Judgment s -> InferT s m NixString
fromValue Judgment s
_ = forall a t. (HasCallStack, IsText t) => t -> a
error Text
"Unused"
instance
MonadInfer m
=> FromValue ( AttrSet (Judgment s)
, PositionSet
) (InferT s m) (Judgment s)
where
fromValueMay :: Judgment s
-> InferT s m (Maybe (AttrSet (Judgment s), PositionSet))
fromValueMay (Judgment Assumption
_ [Constraint]
_ (TSet Variadic
_ AttrSet Type
xs)) =
do
let sing :: b -> Type -> Judgment s
sing = forall a b. a -> b -> a
const forall s. Type -> Judgment s
inferred
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey forall {b} {s}. b -> Type -> Judgment s
sing AttrSet Type
xs, forall a. Monoid a => a
mempty)
fromValueMay Judgment s
_ = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
fromValue :: Judgment s -> InferT s m (AttrSet (Judgment s), PositionSet)
fromValue =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall m. Monoid m => Maybe m -> m
maybeToMonoid
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *) v. FromValue a m v => v -> m (Maybe a)
fromValueMay
foldInitializedWith :: (Traversable t, Applicative f) => (t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith :: forall (t :: * -> *) (f :: * -> *) c b a.
(Traversable t, Applicative f) =>
(t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith t c -> c
fld b -> c
getter a -> f b
init =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t c -> c
fld forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
getter forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
init)
toJudgment :: forall t m s . (Traversable t, Monad m) => (t Type -> Type) -> t (Judgment s) -> InferT s m (Judgment s)
toJudgment :: forall (t :: * -> *) (m :: * -> *) s.
(Traversable t, Monad m) =>
(t Type -> Type) -> t (Judgment s) -> InferT s m (Judgment s)
toJudgment t Type -> Type
c t (Judgment s)
xs =
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall s. Judgment s -> Assumption
assumptions )
(forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall s. Judgment s -> [Constraint]
typeConstraints)
(forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t Type -> Type
c forall s. Judgment s -> Type
inferredType )
where
foldWith :: (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith :: forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t a -> a
g Judgment s -> a
f = forall (t :: * -> *) (f :: * -> *) c b a.
(Traversable t, Applicative f) =>
(t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith t a -> a
g Judgment s -> a
f forall v (m :: * -> *). MonadValue v m => v -> m v
demand t (Judgment s)
xs
instance MonadInfer m
=> ToValue (AttrSet (Judgment s), PositionSet)
(InferT s m) (Judgment s) where
toValue :: (AttrSet (Judgment s), PositionSet) -> InferT s m (Judgment s)
toValue :: (AttrSet (Judgment s), PositionSet) -> InferT s m (Judgment s)
toValue (AttrSet (Judgment s)
xs, PositionSet
_) = forall (t :: * -> *) (m :: * -> *) s.
(Traversable t, Monad m) =>
(t Type -> Type) -> t (Judgment s) -> InferT s m (Judgment s)
toJudgment (Variadic -> AttrSet Type -> Type
TSet Variadic
Variadic) AttrSet (Judgment s)
xs
instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
toValue :: [Judgment s] -> InferT s m (Judgment s)
toValue = forall (t :: * -> *) (m :: * -> *) s.
(Traversable t, Monad m) =>
(t Type -> Type) -> t (Judgment s) -> InferT s m (Judgment s)
toJudgment [Type] -> Type
TList
instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
toValue :: Bool -> InferT s m (Judgment s)
toValue Bool
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall s. Type -> Judgment s
inferred Type
typeBool
instance
Monad m
=> Scoped (Judgment s) (InferT s m) where
askScopes :: InferT s m (Scopes (InferT s m) (Judgment s))
askScopes = forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
m (Scopes m a)
askScopesReader
clearScopes :: forall r. InferT s m r -> InferT s m r
clearScopes = forall (m :: * -> *) a e r.
(MonadReader e m, Has e (Scopes m a)) =>
m r -> m r
clearScopesReader @(InferT s m) @(Judgment s)
pushScopes :: forall r.
Scopes (InferT s m) (Judgment s) -> InferT s m r -> InferT s m r
pushScopes = forall e (m :: * -> *) a r.
(MonadReader e m, Has e (Scopes m a)) =>
Scopes m a -> m r -> m r
pushScopesReader
lookupVar :: VarName -> InferT s m (Maybe (Judgment s))
lookupVar = forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
VarName -> m (Maybe a)
lookupVarReader
instance Monad m => MonadValue (Judgment s) (InferT s m) where
defer
:: InferT s m (Judgment s)
-> InferT s m (Judgment s)
defer :: InferT s m (Judgment s) -> InferT s m (Judgment s)
defer = forall a. a -> a
id
demand
:: Judgment s
-> InferT s m (Judgment s)
demand :: Judgment s -> InferT s m (Judgment s)
demand = forall (f :: * -> *) a. Applicative f => a -> f a
pure
inform
:: Judgment s
-> InferT s m (Judgment s)
inform :: Judgment s -> InferT s m (Judgment s)
inform = forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance Monad m => MonadValueF (Judgment s) (InferT s m) where
demandF
:: ( Judgment s
-> InferT s m r)
-> Judgment s
-> InferT s m r
demandF :: forall r.
(Judgment s -> InferT s m r) -> Judgment s -> InferT s m r
demandF Judgment s -> InferT s m r
f = Judgment s -> InferT s m r
f
informF
:: ( InferT s m (Judgment s)
-> InferT s m (Judgment s)
)
-> Judgment s
-> InferT s m (Judgment s)
informF :: (InferT s m (Judgment s) -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
informF InferT s m (Judgment s) -> InferT s m (Judgment s)
f = InferT s m (Judgment s) -> InferT s m (Judgment s)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
polymorphicVar :: MonadInfer m => VarName -> InferT s m (Judgment s)
polymorphicVar :: forall (m :: * -> *) s.
MonadInfer m =>
VarName -> InferT s m (Judgment s)
polymorphicVar VarName
var =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
(forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ (forall s. Assumption -> [Constraint] -> Type -> Judgment s
`Judgment` forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall x. One x => OneItem x -> x
one VarName
var)
forall (m :: * -> *). MonadState InferState m => m Type
fresh
constInfer :: Applicative f => Type -> b -> f (Judgment s)
constInfer :: forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
x = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall s. Type -> Judgment s
inferred Type
x
instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
freeVariable :: VarName -> InferT s m (Judgment s)
freeVariable = forall (m :: * -> *) s.
MonadInfer m =>
VarName -> InferT s m (Judgment s)
polymorphicVar
synHole :: VarName -> InferT s m (Judgment s)
synHole = forall (m :: * -> *) s.
MonadInfer m =>
VarName -> InferT s m (Judgment s)
polymorphicVar
attrMissing :: NonEmpty VarName -> Maybe (Judgment s) -> InferT s m (Judgment s)
attrMissing NonEmpty VarName
_ Maybe (Judgment s)
_ = forall s. Type -> Judgment s
inferred forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState InferState m => m Type
fresh
evaledSym :: VarName -> Judgment s -> InferT s m (Judgment s)
evaledSym VarName
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
evalCurPos :: InferT s m (Judgment s)
evalCurPos =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall s. Type -> Judgment s
inferred forall a b. (a -> b) -> a -> b
$
Variadic -> AttrSet Type -> Type
TSet forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
[ (VarName
"file", Type
typePath)
, (VarName
"line", Type
typeInt )
, (VarName
"col" , Type
typeInt )
]
evalConstant :: NAtom -> InferT s m (Judgment s)
evalConstant NAtom
c = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall s. Type -> Judgment s
inferred forall a b. (a -> b) -> a -> b
$ NAtom -> Type
fun NAtom
c
where
fun :: NAtom -> Type
fun = \case
NURI Text
_ -> Type
typeString
NInt Integer
_ -> Type
typeInt
NFloat Float
_ -> Type
typeFloat
NBool Bool
_ -> Type
typeBool
NAtom
NNull -> Type
typeNull
evalString :: NString (InferT s m (Judgment s)) -> InferT s m (Judgment s)
evalString = forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
typeString
evalLiteralPath :: Path -> InferT s m (Judgment s)
evalLiteralPath = forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
typePath
evalEnvPath :: Path -> InferT s m (Judgment s)
evalEnvPath = forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
typePath
evalUnary :: NUnaryOp -> Judgment s -> InferT s m (Judgment s)
evalUnary NUnaryOp
op (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) =
(forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
as1 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Constraint]
cs1 forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> NUnaryOp -> [Constraint]
`unops` NUnaryOp
op) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type
t1 Type -> Type -> Type
:~>)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState InferState m => m Type
fresh
evalBinary :: NBinaryOp
-> Judgment s -> InferT s m (Judgment s) -> InferT s m (Judgment s)
evalBinary NBinaryOp
op (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) InferT s m (Judgment s)
e2 =
do
Judgment Assumption
as2 [Constraint]
cs2 Type
t2 <- InferT s m (Judgment s)
e2
(forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment (Assumption
as1 forall a. Semigroup a => a -> a -> a
<> Assumption
as2) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (([Constraint]
cs1 forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2) forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> NBinaryOp -> [Constraint]
`binops` NBinaryOp
op) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Type
t1 Type -> Type -> Type
:~> Type
t2) Type -> Type -> Type
:~>)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState InferState m => m Type
fresh
evalWith :: InferT s m (Judgment s)
-> InferT s m (Judgment s) -> InferT s m (Judgment s)
evalWith = forall v (m :: * -> *). MonadNixEval v m => m v -> m v -> m v
Eval.evalWithAttrSet
evalIf :: Judgment s
-> InferT s m (Judgment s)
-> InferT s m (Judgment s)
-> InferT s m (Judgment s)
evalIf (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) InferT s m (Judgment s)
t InferT s m (Judgment s)
f = do
Judgment Assumption
as2 [Constraint]
cs2 Type
t2 <- InferT s m (Judgment s)
t
Judgment Assumption
as3 [Constraint]
cs3 Type
t3 <- InferT s m (Judgment s)
f
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(Assumption
as1 forall a. Semigroup a => a -> a -> a
<> Assumption
as2 forall a. Semigroup a => a -> a -> a
<> Assumption
as3)
([Constraint]
cs1 forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs3 forall a. Semigroup a => a -> a -> a
<> [Type -> Type -> Constraint
EqConst Type
t1 Type
typeBool, Type -> Type -> Constraint
EqConst Type
t2 Type
t3])
Type
t2
evalAssert :: Judgment s -> InferT s m (Judgment s) -> InferT s m (Judgment s)
evalAssert (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) InferT s m (Judgment s)
body = do
Judgment Assumption
as2 [Constraint]
cs2 Type
t2 <- InferT s m (Judgment s)
body
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(Assumption
as1 forall a. Semigroup a => a -> a -> a
<> Assumption
as2)
([Constraint]
cs1 forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 forall a. Semigroup a => a -> a -> a
<> forall x. One x => OneItem x -> x
one (Type -> Type -> Constraint
EqConst Type
t1 Type
typeBool))
Type
t2
evalApp :: Judgment s -> InferT s m (Judgment s) -> InferT s m (Judgment s)
evalApp (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) InferT s m (Judgment s)
e2 = do
Judgment Assumption
as2 [Constraint]
cs2 Type
t2 <- InferT s m (Judgment s)
e2
Type
tv <- forall (m :: * -> *). MonadState InferState m => m Type
fresh
pure $
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(Assumption
as1 forall a. Semigroup a => a -> a -> a
<> Assumption
as2)
([Constraint]
cs1 forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 forall a. Semigroup a => a -> a -> a
<> forall x. One x => OneItem x -> x
one (Type -> Type -> Constraint
EqConst Type
t1 (Type
t2 Type -> Type -> Type
:~> Type
tv)))
Type
tv
evalAbs :: Params (InferT s m (Judgment s))
-> (forall a.
InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s) -> InferT s m (a, Judgment s))
-> InferT s m (a, Judgment s))
-> InferT s m (Judgment s)
evalAbs (Param VarName
x) forall a.
InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s) -> InferT s m (a, Judgment s))
-> InferT s m (a, Judgment s)
k = do
TVar
a <- forall (m :: * -> *). MonadState InferState m => m TVar
freshTVar
let tv :: Type
tv = TVar -> Type
TVar TVar
a
((), Judgment Assumption
as [Constraint]
cs Type
t) <-
forall s (m :: * -> *) a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet
TVar
a
forall a b. (a -> b) -> a -> b
$ forall a.
InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s) -> InferT s m (a, Judgment s))
-> InferT s m (a, Judgment s)
k
(forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((forall s. Assumption -> [Constraint] -> Type -> Judgment s
`Judgment` forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall x. One x => OneItem x -> x
one VarName
x ) Type
tv))
forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Monoid a => a
mempty,)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(Assumption
as Assumption -> VarName -> Assumption
`Assumption.remove` VarName
x)
([Constraint]
cs forall a. Semigroup a => a -> a -> a
<> [ Type -> Type -> Constraint
EqConst Type
t' Type
tv | Type
t' <- VarName -> Assumption -> [Type]
Assumption.lookup VarName
x Assumption
as ])
(Type
tv Type -> Type -> Type
:~> Type
t)
evalAbs (ParamSet Maybe VarName
_mname Variadic
variadic ParamSet (InferT s m (Judgment s))
pset) forall a.
InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s) -> InferT s m (a, Judgment s))
-> InferT s m (a, Judgment s)
k = do
[(VarName, Type)]
js <- forall (t :: * -> *) (f :: * -> *) c b a.
(Traversable t, Applicative f) =>
(t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall x. One x => OneItem x -> x
one forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, MonadState InferState f) =>
t a -> f (t Type)
intoFresh ParamSet (InferT s m (Judgment s))
pset
let
f :: (a, HashMap k v) -> (k, v) -> (a, HashMap k v)
f (a
as1, HashMap k v
t1) (k
k, v
t) = (a
as1 forall a. Semigroup a => a -> a -> a
<> forall x. One x => OneItem x -> x
one (k
k, v
t), forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert k
k v
t HashMap k v
t1)
(Assumption
env, AttrSet Type
tys) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {a} {k} {v}.
(OneItem a ~ (k, v), Semigroup a, One a, Hashable k) =>
(a, HashMap k v) -> (k, v) -> (a, HashMap k v)
f forall a. Monoid a => a
mempty [(VarName, Type)]
js
arg :: InferT s m (Judgment s)
arg = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
env forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ Variadic -> AttrSet Type -> Type
TSet Variadic
Variadic AttrSet Type
tys
call :: InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
call = forall a.
InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s) -> InferT s m (a, Judgment s))
-> InferT s m (a, Judgment s)
k InferT s m (Judgment s)
arg forall a b. (a -> b) -> a -> b
$ \AttrSet (InferT s m (Judgment s))
args InferT s m (Judgment s)
b -> (AttrSet (InferT s m (Judgment s))
args, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferT s m (Judgment s)
b
names :: [VarName]
names = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VarName, Type)]
js
(AttrSet (InferT s m (Judgment s))
args, Judgment Assumption
as [Constraint]
cs Type
t) <- forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall s (m :: * -> *) a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (TVar TVar
a) -> TVar
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
call [(VarName, Type)]
js
Type
ty <- forall (t :: * -> *) (f :: * -> *) c b a.
(Traversable t, Applicative f) =>
(t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith (Variadic -> AttrSet Type -> Type
TSet Variadic
variadic) forall s. Judgment s -> Type
inferredType forall a. a -> a
id AttrSet (InferT s m (Judgment s))
args
pure $
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
(forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Assumption -> VarName -> Assumption
Assumption.remove Assumption
as [VarName]
names)
([Constraint]
cs forall a. Semigroup a => a -> a -> a
<> [ Type -> Type -> Constraint
EqConst Type
t' (AttrSet Type
tys forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! VarName
x) | VarName
x <- [VarName]
names, Type
t' <- VarName -> Assumption -> [Type]
Assumption.lookup VarName
x Assumption
as ])
(Type
ty Type -> Type -> Type
:~> Type
t)
evalError :: forall s a. Exception s => s -> InferT s m a
evalError = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Exception s => s -> InferError
EvaluationError
class FreeTypeVars a where
ftv :: a -> Set.Set TVar
occursCheck :: FreeTypeVars a => TVar -> a -> Bool
occursCheck :: forall a. FreeTypeVars a => TVar -> a -> Bool
occursCheck TVar
a a
t = TVar
a forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. FreeTypeVars a => a -> Set TVar
ftv a
t
instance FreeTypeVars Type where
ftv :: Type -> Set TVar
ftv TCon{} = forall a. Monoid a => a
mempty
ftv (TVar TVar
a ) = forall x. One x => OneItem x -> x
one TVar
a
ftv (TSet Variadic
_ AttrSet Type
a ) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. FreeTypeVars a => a -> Set TVar
ftv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [v]
M.elems AttrSet Type
a
ftv (TList [Type]
a ) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. FreeTypeVars a => a -> Set TVar
ftv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
a
ftv (Type
t1 :~> Type
t2) = forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 forall a. Semigroup a => a -> a -> a
<> forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2
ftv (TMany [Type]
ts ) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. FreeTypeVars a => a -> Set TVar
ftv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts
instance FreeTypeVars TVar where
ftv :: TVar -> Set TVar
ftv = forall x. One x => OneItem x -> x
one
instance FreeTypeVars Scheme where
ftv :: Scheme -> Set TVar
ftv (Forall [TVar]
as Type
t) = forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. Ord a => [a] -> Set a
Set.fromList [TVar]
as
instance FreeTypeVars a => FreeTypeVars [a] where
ftv :: [a] -> Set TVar
ftv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FreeTypeVars a => a -> Set TVar
ftv) forall a. Monoid a => a
mempty
instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
ftv :: Set a -> Set TVar
ftv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FreeTypeVars a => a -> Set TVar
ftv) forall a. Monoid a => a
mempty
class ActiveTypeVars a where
atv :: a -> Set.Set TVar
instance ActiveTypeVars Constraint where
atv :: Constraint -> Set TVar
atv (EqConst Type
t1 Type
t2 ) = forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 forall a. Semigroup a => a -> a -> a
<> forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2
atv (ImpInstConst Type
t1 Set TVar
ms Type
t2) = forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 forall a. Semigroup a => a -> a -> a
<> (forall a. FreeTypeVars a => a -> Set TVar
ftv Set TVar
ms forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2)
atv (ExpInstConst Type
t Scheme
s ) = forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t forall a. Semigroup a => a -> a -> a
<> forall a. FreeTypeVars a => a -> Set TVar
ftv Scheme
s
instance ActiveTypeVars a => ActiveTypeVars [a] where
atv :: [a] -> Set TVar
atv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ActiveTypeVars a => a -> Set TVar
atv) forall a. Monoid a => a
mempty
type MonadInfer m
= (
MonadAtomicRef m, MonadFix m)
runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
runInfer' :: forall (m :: * -> *) s a.
MonadInfer m =>
InferT s m a -> m (Either InferError a)
runInfer' =
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` InferState
initInfer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` forall a. Monoid a => a
mempty)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. InferT s m a -> InferTInternals s m a
getInfer
runInfer :: (forall s . InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer :: forall a.
(forall s. InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer forall s. InferT s (FreshIdT Int (ST s)) a
m =
forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) i a.
Functor m =>
FreshIdT i m a -> Ref m i -> m a
runFreshIdT (forall (m :: * -> *) s a.
MonadInfer m =>
InferT s m a -> m (Either InferError a)
runInfer' forall s. InferT s (FreshIdT Int (ST s)) a
m) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newRef (Int
1 :: Int)
inferType
:: forall s m . MonadInfer m => Env -> NExpr -> InferT s m [(Subst, Type)]
inferType :: forall s (m :: * -> *).
MonadInfer m =>
Env -> NExpr -> InferT s m [(Subst, Type)]
inferType Env
env NExpr
ex =
do
Judgment Assumption
as [Constraint]
cs Type
t <- forall (m :: * -> *) s.
MonadInfer m =>
NExpr -> InferT s m (Judgment s)
infer NExpr
ex
let
unbounds :: Set VarName
unbounds :: Set VarName
unbounds =
(forall a. Ord a => Set a -> Set a -> Set a
Set.difference forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Ord a => [a] -> Set a
Set.fromList)
(Assumption -> [VarName]
Assumption.keys Assumption
as )
( Env -> [VarName]
Env.keys Env
env)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
(forall (t :: * -> *) a. Foldable t => t a -> Bool
isPresent Set VarName
unbounds)
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadError InferError m => TypeError -> m ()
typeError forall a b. (a -> b) -> a -> b
$ [VarName] -> TypeError
UnboundVariables forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
ordNub forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set VarName
unbounds
InferState
inferState <- forall s (m :: * -> *). MonadState s m => m s
get
let
cs' :: [Constraint]
cs' =
[ Type -> Scheme -> Constraint
ExpInstConst Type
t Scheme
s
| (VarName
x, [Scheme]
ss) <- Env -> [(VarName, [Scheme])]
Env.toList Env
env
, Scheme
s <- [Scheme]
ss
, Type
t <- VarName -> Assumption -> [Type]
Assumption.lookup VarName
x Assumption
as
]
evalResult :: Either [TypeError] [(Subst, Type)]
evalResult =
(forall s a. State s a -> s -> a
`evalState` InferState
inferState) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
Monad m =>
Solver m a -> m (Either [TypeError] [a])
runSolver forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. Substitutable a => Subst -> a -> a
`apply` Type
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve ([Constraint]
cs forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs')
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeError] -> InferError
TypeInferenceErrors)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Either [TypeError] [(Subst, Type)]
evalResult
inferExpr :: Env -> NExpr -> Either InferError [Scheme]
inferExpr :: Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex =
Type -> Scheme
closeOver forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Substitutable a => Subst -> a -> a
apply forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> f (g a) -> f (g b)
<<$>> forall a.
(forall s. InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer (forall s (m :: * -> *).
MonadInfer m =>
Env -> NExpr -> InferT s m [(Subst, Type)]
inferType Env
env NExpr
ex)
unops :: Type -> NUnaryOp -> [Constraint]
unops :: Type -> NUnaryOp -> [Constraint]
unops Type
u1 NUnaryOp
op =
forall x. One x => OneItem x -> x
one forall a b. (a -> b) -> a -> b
$
Type -> Type -> Constraint
EqConst Type
u1 forall a b. (a -> b) -> a -> b
$
case NUnaryOp
op of
NUnaryOp
NNot -> Type -> Type
mkUnaryConstr Type
typeBool
NUnaryOp
NNeg -> [Type] -> Type
TMany forall a b. (a -> b) -> a -> b
$ Type -> Type
mkUnaryConstr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type
typeInt, Type
typeFloat]
where
mkUnaryConstr :: Type -> Type
mkUnaryConstr :: Type -> Type
mkUnaryConstr = NonEmpty Type -> Type
typeFun forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NonEmpty a
mk2same
where
mk2same :: a -> NonEmpty a
mk2same :: forall a. a -> NonEmpty a
mk2same a
a = a
a forall a. a -> [a] -> NonEmpty a
:| forall x. One x => OneItem x -> x
one a
a
binops :: Type -> NBinaryOp -> [Constraint]
binops :: Type -> NBinaryOp -> [Constraint]
binops Type
u1 NBinaryOp
op =
if
| NBinaryOp
op forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NEq , NBinaryOp
NNEq ] -> forall a. Monoid a => a
mempty
| NBinaryOp
op forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NGt , NBinaryOp
NGte , NBinaryOp
NLt , NBinaryOp
NLte ] -> [Constraint]
inequality
| NBinaryOp
op forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NAnd , NBinaryOp
NOr , NBinaryOp
NImpl ] -> [Constraint]
gate
| NBinaryOp
op forall a. Eq a => a -> a -> Bool
== NBinaryOp
NConcat -> [Constraint]
concatenation
| NBinaryOp
op forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NMinus, NBinaryOp
NMult, NBinaryOp
NDiv ] -> [Constraint]
arithmetic
| NBinaryOp
op forall a. Eq a => a -> a -> Bool
== NBinaryOp
NUpdate -> [Constraint]
rUnion
| NBinaryOp
op forall a. Eq a => a -> a -> Bool
== NBinaryOp
NPlus -> [Constraint]
addition
| Bool
otherwise -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"GHC so far can not infer that this pattern match is full, so make it happy."
where
mk3 :: a -> a -> a -> NonEmpty a
mk3 :: forall a. a -> a -> a -> NonEmpty a
mk3 a
a a
b a
c = a
a forall a. a -> [a] -> NonEmpty a
:| [a
b, a
c]
mk3same :: a -> NonEmpty a
mk3same :: forall a. a -> NonEmpty a
mk3same a
a = a
a forall a. a -> [a] -> NonEmpty a
:| [a
a, a
a]
allConst :: Type -> [Constraint]
allConst :: Type -> [Constraint]
allConst = forall x. One x => OneItem x -> x
one forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Constraint
EqConst Type
u1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Type -> Type
typeFun forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NonEmpty a
mk3same
gate :: [Constraint]
gate = Type -> [Constraint]
allConst Type
typeBool
concatenation :: [Constraint]
concatenation = Type -> [Constraint]
allConst Type
typeList
eqConstrMtx :: [NonEmpty Type] -> [Constraint]
eqConstrMtx :: [NonEmpty Type] -> [Constraint]
eqConstrMtx = forall x. One x => OneItem x -> x
one forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Constraint
EqConst Type
u1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
TMany forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty Type -> Type
typeFun
inequality :: [Constraint]
inequality =
[NonEmpty Type] -> [Constraint]
eqConstrMtx
[ forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt Type
typeInt Type
typeBool
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeFloat Type
typeBool
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt Type
typeFloat Type
typeBool
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeInt Type
typeBool
]
arithmetic :: [Constraint]
arithmetic =
[NonEmpty Type] -> [Constraint]
eqConstrMtx
[ forall a. a -> NonEmpty a
mk3same Type
typeInt
, forall a. a -> NonEmpty a
mk3same Type
typeFloat
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt Type
typeFloat Type
typeFloat
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeInt Type
typeFloat
]
rUnion :: [Constraint]
rUnion =
[NonEmpty Type] -> [Constraint]
eqConstrMtx
[ forall a. a -> NonEmpty a
mk3same Type
typeSet
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeSet Type
typeNull Type
typeSet
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeNull Type
typeSet Type
typeSet
]
addition :: [Constraint]
addition =
[NonEmpty Type] -> [Constraint]
eqConstrMtx
[ forall a. a -> NonEmpty a
mk3same Type
typeInt
, forall a. a -> NonEmpty a
mk3same Type
typeFloat
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt Type
typeFloat Type
typeFloat
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeInt Type
typeFloat
, forall a. a -> NonEmpty a
mk3same Type
typeString
, forall a. a -> NonEmpty a
mk3same Type
typePath
, forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeString Type
typeString Type
typePath
]
liftInfer :: Monad m => m a -> InferT s m a
liftInfer :: forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer = forall s (m :: * -> *) a. InferTInternals s m a -> InferT s m a
InferT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
infer :: MonadInfer m => NExpr -> InferT s m (Judgment s)
infer :: forall (m :: * -> *) s.
MonadInfer m =>
NExpr -> InferT s m (Judgment s)
infer = forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix forall v (m :: * -> *). MonadNixEval v m => NExprF (m v) -> m v
Eval.eval
inferTop :: Env -> [(VarName, NExpr)] -> Either InferError Env
inferTop :: Env -> [(VarName, NExpr)] -> Either InferError Env
inferTop Env
env [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
inferTop Env
env ((VarName
name, NExpr
ex) : [(VarName, NExpr)]
xs) =
(\ [Scheme]
ty -> Env -> [(VarName, NExpr)] -> Either InferError Env
inferTop (Env -> (VarName, [Scheme]) -> Env
extend Env
env (VarName
name, [Scheme]
ty)) [(VarName, NExpr)]
xs)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex
newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a)
deriving (forall a b. a -> Solver m b -> Solver m a
forall a b. (a -> b) -> Solver m a -> Solver m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) a b. a -> Solver m b -> Solver m a
forall (m :: * -> *) a b. (a -> b) -> Solver m a -> Solver m b
<$ :: forall a b. a -> Solver m b -> Solver m a
$c<$ :: forall (m :: * -> *) a b. a -> Solver m b -> Solver m a
fmap :: forall a b. (a -> b) -> Solver m a -> Solver m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> Solver m a -> Solver m b
Functor, forall a. a -> Solver m a
forall a b. Solver m a -> Solver m b -> Solver m a
forall a b. Solver m a -> Solver m b -> Solver m b
forall a b. Solver m (a -> b) -> Solver m a -> Solver m b
forall a b c.
(a -> b -> c) -> Solver m a -> Solver m b -> Solver m c
forall (m :: * -> *). Functor (Solver m)
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
forall (m :: * -> *) a. a -> Solver m a
forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m a
forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m b
forall (m :: * -> *) a b.
Solver m (a -> b) -> Solver m a -> Solver m b
forall (m :: * -> *) a b c.
(a -> b -> c) -> Solver m a -> Solver m b -> Solver m c
<* :: forall a b. Solver m a -> Solver m b -> Solver m a
$c<* :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m a
*> :: forall a b. Solver m a -> Solver m b -> Solver m b
$c*> :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m b
liftA2 :: forall a b c.
(a -> b -> c) -> Solver m a -> Solver m b -> Solver m c
$cliftA2 :: forall (m :: * -> *) a b c.
(a -> b -> c) -> Solver m a -> Solver m b -> Solver m c
<*> :: forall a b. Solver m (a -> b) -> Solver m a -> Solver m b
$c<*> :: forall (m :: * -> *) a b.
Solver m (a -> b) -> Solver m a -> Solver m b
pure :: forall a. a -> Solver m a
$cpure :: forall (m :: * -> *) a. a -> Solver m a
Applicative, forall a. Solver m a
forall a. Solver m a -> Solver m [a]
forall a. Solver m a -> Solver m a -> Solver m a
forall (m :: * -> *). Applicative (Solver m)
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) a. Solver m a
forall (m :: * -> *) a. Solver m a -> Solver m [a]
forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
many :: forall a. Solver m a -> Solver m [a]
$cmany :: forall (m :: * -> *) a. Solver m a -> Solver m [a]
some :: forall a. Solver m a -> Solver m [a]
$csome :: forall (m :: * -> *) a. Solver m a -> Solver m [a]
<|> :: forall a. Solver m a -> Solver m a -> Solver m a
$c<|> :: forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
empty :: forall a. Solver m a
$cempty :: forall (m :: * -> *) a. Solver m a
Alternative, forall a. a -> Solver m a
forall a b. Solver m a -> Solver m b -> Solver m b
forall a b. Solver m a -> (a -> Solver m b) -> Solver m b
forall (m :: * -> *). Applicative (Solver m)
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
forall (m :: * -> *) a. a -> Solver m a
forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m b
forall (m :: * -> *) a b.
Solver m a -> (a -> Solver m b) -> Solver m b
return :: forall a. a -> Solver m a
$creturn :: forall (m :: * -> *) a. a -> Solver m a
>> :: forall a b. Solver m a -> Solver m b -> Solver m b
$c>> :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m b
>>= :: forall a b. Solver m a -> (a -> Solver m b) -> Solver m b
$c>>= :: forall (m :: * -> *) a b.
Solver m a -> (a -> Solver m b) -> Solver m b
Monad, forall a. Solver m a
forall a. Solver m a -> Solver m a -> Solver m a
forall (m :: * -> *). Monad (Solver m)
forall (m :: * -> *). Alternative (Solver m)
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
forall (m :: * -> *) a. Solver m a
forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
mplus :: forall a. Solver m a -> Solver m a -> Solver m a
$cmplus :: forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
mzero :: forall a. Solver m a
$cmzero :: forall (m :: * -> *) a. Solver m a
MonadPlus,
forall a. Solver m a -> Solver m a
forall a. Solver m a -> Solver m (Maybe (a, Solver m a))
forall a. Solver m a -> Solver m ()
forall a. Solver m a -> Solver m a -> Solver m a
forall a b. Solver m a -> (a -> Solver m b) -> Solver m b
forall a b.
Solver m a -> (a -> Solver m b) -> Solver m b -> Solver m b
forall {m :: * -> *}. Monad m => Monad (Solver m)
forall {m :: * -> *}. Monad m => Alternative (Solver m)
forall (m :: * -> *).
Monad m
-> Alternative m
-> (forall a. m a -> m (Maybe (a, m a)))
-> (forall a. m a -> m a -> m a)
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a. m a -> m a)
-> (forall a. m a -> m ())
-> (forall a b. m a -> (a -> m b) -> m b -> m b)
-> MonadLogic m
forall (m :: * -> *) a. Monad m => Solver m a -> Solver m a
forall (m :: * -> *) a.
Monad m =>
Solver m a -> Solver m (Maybe (a, Solver m a))
forall (m :: * -> *) a. Monad m => Solver m a -> Solver m ()
forall (m :: * -> *) a.
Monad m =>
Solver m a -> Solver m a -> Solver m a
forall (m :: * -> *) a b.
Monad m =>
Solver m a -> (a -> Solver m b) -> Solver m b
forall (m :: * -> *) a b.
Monad m =>
Solver m a -> (a -> Solver m b) -> Solver m b -> Solver m b
ifte :: forall a b.
Solver m a -> (a -> Solver m b) -> Solver m b -> Solver m b
$cifte :: forall (m :: * -> *) a b.
Monad m =>
Solver m a -> (a -> Solver m b) -> Solver m b -> Solver m b
lnot :: forall a. Solver m a -> Solver m ()
$clnot :: forall (m :: * -> *) a. Monad m => Solver m a -> Solver m ()
once :: forall a. Solver m a -> Solver m a
$conce :: forall (m :: * -> *) a. Monad m => Solver m a -> Solver m a
>>- :: forall a b. Solver m a -> (a -> Solver m b) -> Solver m b
$c>>- :: forall (m :: * -> *) a b.
Monad m =>
Solver m a -> (a -> Solver m b) -> Solver m b
interleave :: forall a. Solver m a -> Solver m a -> Solver m a
$cinterleave :: forall (m :: * -> *) a.
Monad m =>
Solver m a -> Solver m a -> Solver m a
msplit :: forall a. Solver m a -> Solver m (Maybe (a, Solver m a))
$cmsplit :: forall (m :: * -> *) a.
Monad m =>
Solver m a -> Solver m (Maybe (a, Solver m a))
MonadLogic, MonadState [TypeError])
runSolver :: forall m a . Monad m => Solver m a -> m (Either [TypeError] [a])
runSolver :: forall (m :: * -> *) a.
Monad m =>
Solver m a -> m (Either [TypeError] [a])
runSolver (Solver LogicT (StateT [TypeError] m) a
s) =
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [a] -> [TypeError] -> Either [TypeError] [a]
report forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
observeAllT LogicT (StateT [TypeError] m) a
s) forall a. Monoid a => a
mempty
where
report :: [a] -> [TypeError] -> Either [TypeError] [a]
report :: [a] -> [TypeError] -> Either [TypeError] [a]
report [a]
xs [TypeError]
e =
forall (t :: * -> *) b a. Foldable t => b -> (t a -> b) -> t a -> b
handlePresence
(forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
ordNub [TypeError]
e)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
[a]
xs
instance MonadTrans Solver where
lift :: forall (m :: * -> *) a. Monad m => m a -> Solver m a
lift = forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
instance Monad m => MonadError TypeError (Solver m) where
throwError :: forall a. TypeError -> Solver m a
throwError TypeError
err = forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (TypeError
err forall a. a -> [a] -> [a]
:)) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall a. Monoid a => a
mempty
catchError :: forall a. Solver m a -> (TypeError -> Solver m a) -> Solver m a
catchError Solver m a
_ TypeError -> Solver m a
_ = forall a t. (HasCallStack, IsText t) => t -> a
error Text
"This is never used"
bind :: Monad m => TVar -> Type -> Solver m Subst
bind :: forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
bind TVar
a Type
t | Type
t forall a. Eq a => a -> a -> Bool
== TVar -> Type
TVar TVar
a = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
| forall a. FreeTypeVars a => TVar -> a -> Bool
occursCheck TVar
a Type
t = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TVar -> Type -> TypeError
InfiniteType TVar
a Type
t
| Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Map TVar Type -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall x. One x => OneItem x -> x
one (TVar
a, Type
t)
considering :: [a] -> Solver m a
considering :: forall a (m :: * -> *). [a] -> Solver m a
considering [a]
xs = forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \a -> StateT [TypeError] m r -> StateT [TypeError] m r
c StateT [TypeError] m r
n -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> StateT [TypeError] m r -> StateT [TypeError] m r
c StateT [TypeError] m r
n [a]
xs
unifies :: Monad m => Type -> Type -> Solver m Subst
unifies :: forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2 | Type
t1 forall a. Eq a => a -> a -> Bool
== Type
t2 = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TVar TVar
v) Type
t = TVar
v forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
`bind` Type
t
unifies Type
t (TVar TVar
v) = TVar
v forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
`bind` Type
t
unifies (TList [Type]
xs) (TList [Type]
ys)
| [Type] -> Bool
allSameType [Type]
xs Bool -> Bool -> Bool
&& [Type] -> Bool
allSameType [Type]
ys =
case ([Type]
xs, [Type]
ys) of
(Type
x : [Type]
_, Type
y : [Type]
_) -> forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
x Type
y
([Type], [Type])
_ -> forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ys = forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany [Type]
xs [Type]
ys
unifies t1 :: Type
t1@(TList [Type]
_ ) t2 :: Type
t2@(TList [Type]
_ ) = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
UnificationFail Type
t1 Type
t2
unifies (TSet Variadic
Variadic AttrSet Type
_) (TSet Variadic
Variadic AttrSet Type
_) = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TSet Variadic
Closed AttrSet Type
s) (TSet Variadic
Closed AttrSet Type
b) | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b forall a. Eq a => [a] -> [a] -> [a]
\\ forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s) = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TSet Variadic
_ AttrSet Type
a) (TSet Variadic
_ AttrSet Type
b) | (forall k v. HashMap k v -> [k]
M.keys AttrSet Type
a forall a. Eq a => [a] -> [a] -> [a]
`intersect` forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b) forall a. Eq a => a -> a -> Bool
== forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (Type
t1 :~> Type
t2) (Type
t3 :~> Type
t4) = forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany [Type
t1, Type
t2] [Type
t3, Type
t4]
unifies (TMany [Type]
t1s) Type
t2 = forall a (m :: * -> *). [a] -> Solver m a
considering [Type]
t1s forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- (forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
`unifies` Type
t2)
unifies Type
t1 (TMany [Type]
t2s) = forall a (m :: * -> *). [a] -> Solver m a
considering [Type]
t2s forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1
unifies Type
t1 Type
t2 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
UnificationFail Type
t1 Type
t2
unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany :: forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany [] [] = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifyMany (Type
t1 : [Type]
ts1) (Type
t2 : [Type]
ts2) =
do
Subst
su1 <- forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2
Subst
su2 <-
(forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Substitutable a => Subst -> a -> a
apply Subst
su1) [Type]
ts1 [Type]
ts2
pure $ Subst -> Subst -> Subst
compose Subst
su1 Subst
su2
unifyMany [Type]
t1 [Type]
t2 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> TypeError
UnificationMismatch [Type]
t1 [Type]
t2
nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Constraint, [Constraint]) -> Bool
solvable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [(a, [a])]
pickFirstOne
where
pickFirstOne :: Eq a => [a] -> [(a, [a])]
pickFirstOne :: forall a. Eq a => [a] -> [(a, [a])]
pickFirstOne [a]
xs = [ (a
x, [a]
ys) | a
x <- [a]
xs, let ys :: [a]
ys = forall a. Eq a => a -> [a] -> [a]
delete a
x [a]
xs ]
solvable :: (Constraint, [Constraint]) -> Bool
solvable :: (Constraint, [Constraint]) -> Bool
solvable (EqConst{} , [Constraint]
_) = Bool
True
solvable (ExpInstConst{}, [Constraint]
_) = Bool
True
solvable (ImpInstConst Type
_t1 Set TVar
ms Type
t2, [Constraint]
cs) =
forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ (Set TVar
ms forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2) forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall a. ActiveTypeVars a => a -> Set TVar
atv [Constraint]
cs
solve :: forall m . MonadState InferState m => [Constraint] -> Solver m Subst
solve :: forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve [] = forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
solve [Constraint]
cs = forall {m :: * -> *}.
MonadState InferState m =>
(Constraint, [Constraint]) -> Solver m Subst
solve' forall a b. (a -> b) -> a -> b
$ [Constraint] -> (Constraint, [Constraint])
nextSolvable [Constraint]
cs
where
solve' :: (Constraint, [Constraint]) -> Solver m Subst
solve' (ImpInstConst Type
t1 Set TVar
ms Type
t2, [Constraint]
cs) =
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve (Type -> Scheme -> Constraint
ExpInstConst Type
t1 (Set TVar -> Type -> Scheme
generalize Set TVar
ms Type
t2) forall a. a -> [a] -> [a]
: [Constraint]
cs)
solve' (ExpInstConst Type
t Scheme
s, [Constraint]
cs) =
do
Type
s' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadState InferState m => Scheme -> m Type
instantiate Scheme
s
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve (Type -> Type -> Constraint
EqConst Type
t Type
s' forall a. a -> [a] -> [a]
: [Constraint]
cs)
solve' (EqConst Type
t1 Type
t2, [Constraint]
cs) =
(\ Subst
su1 ->
(forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Subst -> Subst
compose Subst
su1) forall (m :: * -> *) a b.
Monad m =>
(a -> Solver m b) -> Solver m a -> Solver m b
-<< forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve ((forall a. Substitutable a => Subst -> a -> a
`apply` [Constraint]
cs) Subst
su1)
) forall (m :: * -> *) a b.
Monad m =>
(a -> Solver m b) -> Solver m a -> Solver m b
-<<
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2
infixr 1 -<<
(-<<) :: Monad m => (a -> Solver m b) -> Solver m a -> Solver m b
-<< :: forall (m :: * -> *) a b.
Monad m =>
(a -> Solver m b) -> Solver m a -> Solver m b
(-<<) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
(>>-)