{-# 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     hiding ( fail )
import           Control.Monad.Reader           ( 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 ((TVar, TVar) -> TVar
forall a b. (a, b) -> b
snd ((TVar, TVar) -> TVar) -> [(TVar, TVar)] -> [TVar]
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 =
    [TVar] -> [TVar] -> [(TVar, TVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip
      ([TVar] -> [TVar]
forall a. Ord a => [a] -> [a]
ordNub ([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ Type -> [TVar]
forall m. (One m, Monoid m, OneItem m ~ TVar) => Type -> m
fv Type
body)
      (Text -> TVar
TV (Text -> TVar) -> (String -> Text) -> String -> TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString (String -> TVar) -> [String] -> [TVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
letters)

  fv :: Type -> m
fv (TVar TVar
a  ) = OneItem m -> m
forall x. One x => OneItem x -> x
one OneItem m
TVar
a
  fv (Type
a :~> Type
b ) = (m -> m -> m) -> (Type -> m) -> Type -> Type -> m
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on m -> m -> m
forall a. Semigroup a => a -> a -> a
(<>) Type -> m
fv Type
a Type
b
  fv (TCon Text
_  ) = m
forall a. Monoid a => a
mempty
  fv (TSet Variadic
_ AttrSet Type
a) = (Type -> m) -> [Type] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> m
fv ([Type] -> m) -> [Type] -> m
forall a b. (a -> b) -> a -> b
$ AttrSet Type -> [Type]
forall k v. HashMap k v -> [v]
M.elems AttrSet Type
a
  fv (TList [Type]
a ) = (Type -> m) -> [Type] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> m
fv [Type]
a
  fv (TMany [Type]
ts) = (Type -> m) -> [Type] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> m
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 (AttrSet Type -> Type) -> AttrSet Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype (Type -> Type) -> AttrSet Type -> AttrSet Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrSet Type
a
  normtype (TList [Type]
a ) = [Type] -> Type
TList ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
a
  normtype (TMany [Type]
ts) = [Type] -> Type
TMany ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
normtype (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts
  normtype (TVar  TVar
a ) =
    Type -> (TVar -> Type) -> Maybe TVar -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (Text -> Type
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"type variable not in signature")
      TVar -> Type
TVar
      (TVar -> [(TVar, TVar)] -> Maybe 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 = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar
free Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t

-- | Canonicalize and return the polymorphic toplevel type.
closeOver :: Type -> Scheme
closeOver :: Type -> Scheme
closeOver = Scheme -> Scheme
normalizeScheme (Scheme -> Scheme) -> (Type -> Scheme) -> Type -> Scheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVar -> Type -> Scheme
generalize Set TVar
forall a. Monoid a => a
mempty

-- When `[]` becomes `NonEmpty` - function becomes just `all`
-- | Check if all elements are of the same type.
allSameType :: [Type] -> Bool
allSameType :: [Type] -> Bool
allSameType = [Type] -> Bool
forall a. Eq a => [a] -> Bool
allSame
 where
  allSame :: Eq a => [a] -> Bool
  allSame :: [a] -> Bool
allSame [] = Bool
True
  allSame (a
x:[a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==) [a]
xs

-- * data type @TypeError@

data TypeError
  = UnificationFail Type Type
  | InfiniteType TVar Type
  | UnboundVariables [VarName]
  | Ambigious [Constraint]
  | UnificationMismatch [Type] [Type]
  deriving (TypeError -> TypeError -> Bool
(TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool) -> Eq TypeError
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
(Int -> TypeError -> ShowS)
-> (TypeError -> String)
-> ([TypeError] -> ShowS)
-> Show TypeError
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
Eq TypeError
-> (TypeError -> TypeError -> Ordering)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> TypeError)
-> (TypeError -> TypeError -> TypeError)
-> Ord 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
$cp1Ord :: Eq TypeError
Ord)

-- * @InferError@

data InferError
  = TypeInferenceErrors [TypeError]
  | TypeInferenceAborted
  | forall s. Exception s => EvaluationError s

typeError :: MonadError InferError m => TypeError -> m ()
typeError :: TypeError -> m ()
typeError TypeError
err = InferError -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InferError -> m ()) -> InferError -> m ()
forall a b. (a -> b) -> a -> b
$ [TypeError] -> InferError
TypeInferenceErrors ([TypeError] -> InferError) -> [TypeError] -> InferError
forall a b. (a -> b) -> a -> b
$ OneItem [TypeError] -> [TypeError]
forall x. One x => OneItem x -> x
one OneItem [TypeError]
TypeError
err

-- ** Instances

deriving instance Show InferError
instance Exception InferError

instance Semigroup InferError where
  <> :: InferError -> InferError -> InferError
(<>) = InferError -> InferError -> InferError
forall a b. a -> b -> a
const

instance Monoid InferError where
  mempty :: InferError
mempty  = InferError
TypeInferenceAborted

-- * @InferState@: inference state

-- | Inference state (stage).
newtype InferState = InferState Int
 deriving
  (InferState -> InferState -> Bool
(InferState -> InferState -> Bool)
-> (InferState -> InferState -> Bool) -> Eq InferState
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
(InferState -> InferState -> InferState)
-> (InferState -> InferState -> InferState)
-> (InferState -> InferState -> InferState)
-> (InferState -> InferState)
-> (InferState -> InferState)
-> (InferState -> InferState)
-> (Integer -> InferState)
-> Num 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]
(InferState -> InferState)
-> (InferState -> InferState)
-> (Int -> InferState)
-> (InferState -> Int)
-> (InferState -> [InferState])
-> (InferState -> InferState -> [InferState])
-> (InferState -> InferState -> [InferState])
-> (InferState -> InferState -> InferState -> [InferState])
-> Enum 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
Eq InferState
-> (InferState -> InferState -> Ordering)
-> (InferState -> InferState -> Bool)
-> (InferState -> InferState -> Bool)
-> (InferState -> InferState -> Bool)
-> (InferState -> InferState -> Bool)
-> (InferState -> InferState -> InferState)
-> (InferState -> InferState -> InferState)
-> Ord 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
$cp1Ord :: Eq InferState
Ord)

instance Semigroup InferState where
  <> :: InferState -> InferState -> InferState
(<>) = InferState -> InferState -> InferState
forall a. Num a => a -> a -> a
(+)

instance Monoid InferState where
  mempty :: InferState
mempty = InferState
0

-- | Initial inference state
initInfer :: InferState
initInfer :: InferState
initInfer = Int -> InferState
InferState Int
0

letters :: [String]
letters :: [String]
letters =
  do
    Int
l <- [Int
1 ..]
    Int -> String -> [String]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM
      Int
l
      [Char
'a' .. Char
'z']

freshTVar :: MonadState InferState m => m TVar
freshTVar :: m TVar
freshTVar =
  do
    InferState
s <- m InferState
forall s (m :: * -> *). MonadState s m => m s
get
    InferState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InferState -> m ()) -> InferState -> m ()
forall a b. (a -> b) -> a -> b
$ InferState -> InferState
forall a. Enum a => a -> a
succ InferState
s
    pure $ Text -> TVar
TV (Text -> TVar) -> Text -> TVar
forall a b. (a -> b) -> a -> b
$ String -> Text
forall a. IsString a => String -> a
fromString (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ [String]
letters [String] -> Int -> String
forall a. [a] -> Int -> a
!! InferState -> Int
coerce InferState
s

fresh :: MonadState InferState m => m Type
fresh :: m Type
fresh = TVar -> Type
TVar (TVar -> Type) -> m TVar -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TVar
forall (m :: * -> *). MonadState InferState m => m TVar
freshTVar

intoFresh :: (Traversable t, MonadState InferState f) => t a -> f (t Type)
intoFresh :: t a -> f (t Type)
intoFresh =
  (a -> f Type) -> t a -> f (t Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (f Type -> a -> f Type
forall a b. a -> b -> a
const f Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh)

instantiate :: MonadState InferState m => Scheme -> m Type
instantiate :: Scheme -> m Type
instantiate (Forall [TVar]
as Type
t) =
  ([Type] -> Type) -> m [Type] -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
`apply` Type
t) (Subst -> Type) -> ([Type] -> Subst) -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TVar Type -> Subst
coerce (Map TVar Type -> Subst)
-> ([Type] -> Map TVar Type) -> [Type] -> Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TVar, Type)] -> Map TVar Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, Type)] -> Map TVar Type)
-> ([Type] -> [(TVar, Type)]) -> [Type] -> Map TVar Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TVar] -> [Type] -> [(TVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as) ([TVar] -> m [Type]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, MonadState InferState f) =>
t a -> f (t Type)
intoFresh [TVar]
as)

-- * @Constraint@ data type

data Constraint
  = EqConst Type Type
  | ExpInstConst Type Scheme
  | ImpInstConst Type (Set.Set TVar) Type
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
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
(Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool) -> Eq Constraint
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
Eq Constraint
-> (Constraint -> Constraint -> Ordering)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Constraint)
-> (Constraint -> Constraint -> Constraint)
-> Ord 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
$cp1Ord :: Eq Constraint
Ord)

-- * @Subst@ data type

-- | Substitution of the basic type definition by a type variable.
newtype Subst = Subst (Map TVar Type)
  deriving (Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
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
Eq Subst
-> (Subst -> Subst -> Ordering)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Subst)
-> (Subst -> Subst -> Subst)
-> Ord 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
$cp1Ord :: Eq Subst
Ord, Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
(Int -> Subst -> ShowS)
-> (Subst -> String) -> ([Subst] -> ShowS) -> Show Subst
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, b -> Subst -> Subst
NonEmpty Subst -> Subst
Subst -> Subst -> Subst
(Subst -> Subst -> Subst)
-> (NonEmpty Subst -> Subst)
-> (forall b. Integral b => b -> Subst -> Subst)
-> Semigroup 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 :: 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
Semigroup Subst
-> Subst
-> (Subst -> Subst -> Subst)
-> ([Subst] -> Subst)
-> Monoid 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
$cp1Monoid :: Semigroup Subst
Monoid)

-- | Compose substitutions
compose :: Subst -> Subst -> Subst
compose :: Subst -> Subst -> Subst
compose a :: Subst
a@(Subst Map TVar Type
s2) (Subst Map TVar Type
s1) =
  Map TVar Type -> Subst
coerce (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ --
    Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
a (Type -> Type) -> Map TVar Type -> Map TVar Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      (Map TVar Type
s2 Map TVar Type -> Map TVar Type -> Map TVar Type
forall a. Semigroup a => a -> a -> a
<> Map TVar Type
s1)

-- * class @Substitutable@

class Substitutable a where
  apply :: Subst -> a -> a

-- ** Instances

instance Substitutable TVar where
  apply :: Subst -> TVar -> TVar
apply (Subst Map TVar Type
s) TVar
a = TVar
tv
   where
    (TVar TVar
tv) = Type -> TVar -> Map TVar Type -> Type
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 (AttrSet Type -> Type) -> AttrSet Type -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s (Type -> Type) -> AttrSet Type -> AttrSet Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrSet Type
a
  apply Subst
s         (  TList [Type]
a  ) = [Type] -> Type
TList  ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s (Type -> Type) -> [Type] -> [Type]
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  ) = Type -> TVar -> Map TVar Type -> Type
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
(:~>) (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s) Type
t1 Type
t2
  apply Subst
s         (  TMany [Type]
ts ) = [Type] -> Type
TMany  ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s (Type -> Type) -> [Type] -> [Type]
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 (Type -> Scheme) -> Type -> Scheme
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s' Type
t
   where
    s' :: Subst
s' = Map TVar Type -> Subst
Subst (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ (TVar -> Map TVar Type -> Map TVar Type)
-> Map TVar Type -> [TVar] -> Map TVar Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TVar -> Map TVar Type -> Map TVar Type
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) = (Type -> Type -> Constraint)
-> (Type -> Type) -> Type -> Type -> Constraint
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Type -> Type -> Constraint
EqConst (Subst -> Type -> Type
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
      (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t)
      (Subst -> Scheme -> Scheme
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
      (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t1)
      (Subst -> Set TVar -> Set TVar
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Set TVar
ms)
      (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t2)

instance Substitutable a => Substitutable [a] where
  apply :: Subst -> [a] -> [a]
apply = (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a])
-> (Subst -> a -> a) -> Subst -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
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 = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> a) -> Set a -> Set a)
-> (Subst -> a -> a) -> Subst -> Set a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
forall a. Substitutable a => Subst -> a -> a
apply


-- * data type @Judgment@

data Judgment s =
  Judgment
    { Judgment s -> Assumption
assumptions     :: Assumption
    , Judgment s -> [Constraint]
typeConstraints :: [Constraint]
    , Judgment s -> Type
inferredType    :: Type
    }
    deriving Int -> Judgment s -> ShowS
[Judgment s] -> ShowS
Judgment s -> String
(Int -> Judgment s -> ShowS)
-> (Judgment s -> String)
-> ([Judgment s] -> ShowS)
-> Show (Judgment s)
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 :: Type -> Judgment s
inferred = Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
forall a. Monoid a => a
mempty [Constraint]
forall a. Monoid a => a
mempty

-- * @InferT@: inference monad

type InferTInternals s m a =
  ReaderT
    (Set.Set TVar, Scopes (InferT s m) (Judgment s))
    (StateT InferState (ExceptT InferError m))
    a

-- | Inference monad
newtype InferT s m a =
  InferT
    { InferT s m a -> InferTInternals s m a
getInfer ::
        InferTInternals s m a
    }
    deriving
      ( a -> InferT s m b -> InferT s m a
(a -> b) -> InferT s m a -> InferT s m b
(forall a b. (a -> b) -> InferT s m a -> InferT s m b)
-> (forall a b. a -> InferT s m b -> InferT s m a)
-> Functor (InferT s m)
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
<$ :: 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 :: (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
      , Functor (InferT s m)
a -> InferT s m a
Functor (InferT s m)
-> (forall a. a -> InferT s m a)
-> (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 a b. InferT s m a -> InferT s m b -> InferT s m b)
-> (forall a b. InferT s m a -> InferT s m b -> InferT s m a)
-> Applicative (InferT s m)
InferT s m a -> InferT s m b -> InferT s m b
InferT s m a -> InferT s m b -> InferT s m a
InferT s m (a -> b) -> InferT s m a -> InferT s m b
(a -> b -> c) -> InferT s m a -> InferT s m b -> InferT s m c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> InferT s m a
$cpure :: forall s (m :: * -> *) a. Monad m => a -> InferT s m a
$cp1Applicative :: forall s (m :: * -> *). Monad m => Functor (InferT s m)
Applicative
      , Applicative (InferT s m)
InferT s m a
Applicative (InferT s m)
-> (forall a. InferT s m a)
-> (forall a. InferT s m a -> InferT s m 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])
-> Alternative (InferT s m)
InferT s m a -> InferT s m a -> InferT s m a
InferT s m a -> InferT s m [a]
InferT s m a -> InferT s m [a]
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 :: InferT s m a -> InferT s m [a]
$cmany :: forall s (m :: * -> *) a. Monad m => InferT s m a -> InferT s m [a]
some :: InferT s m a -> InferT s m [a]
$csome :: forall s (m :: * -> *) a. Monad m => InferT s m a -> InferT s m [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 :: InferT s m a
$cempty :: forall s (m :: * -> *) a. Monad m => InferT s m a
$cp1Alternative :: forall s (m :: * -> *). Monad m => Applicative (InferT s m)
Alternative
      , Applicative (InferT s m)
a -> InferT s m a
Applicative (InferT s m)
-> (forall a b.
    InferT s m a -> (a -> InferT s m b) -> InferT s m b)
-> (forall a b. InferT s m a -> InferT s m b -> InferT s m b)
-> (forall a. a -> InferT s m a)
-> Monad (InferT s m)
InferT s m a -> (a -> InferT s m b) -> InferT s m b
InferT s m a -> InferT s m b -> InferT s m b
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 :: a -> InferT s m a
$creturn :: forall s (m :: * -> *) a. Monad m => a -> InferT s m a
>> :: 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
>>= :: 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
$cp1Monad :: forall s (m :: * -> *). Monad m => Applicative (InferT s m)
Monad
      , Monad (InferT s m)
Alternative (InferT s m)
InferT s m a
Alternative (InferT s m)
-> Monad (InferT s m)
-> (forall a. InferT s m a)
-> (forall a. InferT s m a -> InferT s m a -> InferT s m a)
-> MonadPlus (InferT s m)
InferT s m a -> InferT s m a -> InferT s m a
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 :: 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 :: InferT s m a
$cmzero :: forall s (m :: * -> *) a. Monad m => InferT s m a
$cp2MonadPlus :: forall s (m :: * -> *). Monad m => Monad (InferT s m)
$cp1MonadPlus :: forall s (m :: * -> *). Monad m => Alternative (InferT s m)
MonadPlus
      , Monad (InferT s m)
Monad (InferT s m)
-> (forall a. (a -> InferT s m a) -> InferT s m a)
-> MonadFix (InferT s m)
(a -> InferT s m a) -> InferT s m a
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 :: (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
$cp1MonadFix :: forall s (m :: * -> *). MonadFix m => Monad (InferT s m)
MonadFix
      , MonadReader (Set.Set TVar, Scopes (InferT s m) (Judgment s))
      , Monad (InferT s m)
Monad (InferT s m)
-> (forall a. String -> InferT s m a) -> MonadFail (InferT s m)
String -> InferT s m a
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 :: String -> InferT s m a
$cfail :: forall s (m :: * -> *) a. MonadFail m => String -> InferT s m a
$cp1MonadFail :: forall s (m :: * -> *). MonadFail m => Monad (InferT s m)
MonadFail
      , MonadState InferState
      , MonadError InferError
      )

extendMSet :: forall s m a . Monad m => TVar -> InferT s m a -> InferT s m a
extendMSet :: TVar -> InferT s m a -> InferT s m a
extendMSet TVar
x = (InferTInternals s m a -> InferTInternals s m a)
-> InferT s m a -> InferT s m a
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 = ((Set TVar, Scopes (InferT s m) (Judgment s))
 -> (Set TVar, Scopes (InferT s m) (Judgment s)))
-> InferTInternals s m a -> InferTInternals s m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Set TVar -> Set TVar)
-> (Set TVar, Scopes (InferT s m) (Judgment s))
-> (Set TVar, Scopes (InferT s m) (Judgment s))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Set TVar -> Set TVar)
 -> (Set TVar, Scopes (InferT s m) (Judgment s))
 -> (Set TVar, Scopes (InferT s m) (Judgment s)))
-> (TVar -> Set TVar -> Set TVar)
-> TVar
-> (Set TVar, Scopes (InferT s m) (Judgment s))
-> (Set TVar, Scopes (InferT s m) (Judgment s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Set TVar -> Set TVar
forall a. Ord a => a -> Set a -> Set a
Set.insert (TVar
 -> (Set TVar, Scopes (InferT s m) (Judgment s))
 -> (Set TVar, Scopes (InferT s m) (Judgment s)))
-> TVar
-> (Set TVar, Scopes (InferT s m) (Judgment s))
-> (Set TVar, Scopes (InferT s m) (Judgment s))
forall a b. (a -> b) -> a -> b
$ TVar
x)

-- ** Instances

instance MonadTrans (InferT s) where
  lift :: m a -> InferT s m a
lift = InferTInternals s m a -> InferT s m a
forall s (m :: * -> *) a. InferTInternals s m a -> InferT s m a
InferT (InferTInternals s m a -> InferT s m a)
-> (m a -> InferTInternals s m a) -> m a -> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT InferState (ExceptT InferError m) a -> InferTInternals s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT InferState (ExceptT InferError m) a
 -> InferTInternals s m a)
-> (m a -> StateT InferState (ExceptT InferError m) a)
-> m a
-> InferTInternals s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT InferError m a
-> StateT InferState (ExceptT InferError m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT InferError m a
 -> StateT InferState (ExceptT InferError m) a)
-> (m a -> ExceptT InferError m a)
-> m a
-> StateT InferState (ExceptT InferError m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> ExceptT InferError m a
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 :: a -> InferT s m (Ref (InferT s m) a)
newRef a
x = m (Ref m a) -> InferT s m (Ref m a)
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer (m (Ref m a) -> InferT s m (Ref m a))
-> m (Ref m a) -> InferT s m (Ref m a)
forall a b. (a -> b) -> a -> b
$ a -> m (Ref m a)
forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newRef a
x
  readRef :: Ref (InferT s m) a -> InferT s m a
readRef Ref (InferT s m) a
x = m a -> InferT s m a
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer (m a -> InferT s m a) -> m a -> InferT s m a
forall a b. (a -> b) -> a -> b
$ Ref m a -> m a
forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readRef Ref m a
Ref (InferT s m) a
x
  writeRef :: Ref (InferT s m) a -> a -> InferT s m ()
writeRef Ref (InferT s m) a
x a
y = m () -> InferT s m ()
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer (m () -> InferT s m ()) -> m () -> InferT s m ()
forall a b. (a -> b) -> a -> b
$ Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeRef Ref m a
Ref (InferT s m) a
x a
y

instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
  atomicModifyRef :: Ref (InferT s m) a -> (a -> (a, b)) -> InferT s m b
atomicModifyRef Ref (InferT s m) a
x a -> (a, b)
f =
    m b -> InferT s m b
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer (m b -> InferT s m b) -> m b -> InferT s m b
forall a b. (a -> b) -> a -> b
$
      do
        b
res <- (a, b) -> b
forall a b. (a, b) -> b
snd ((a, b) -> b) -> (a -> (a, b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (a, b)
f (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref m a -> m a
forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readRef Ref m a
Ref (InferT s m) a
x
        ()
_   <- Ref m a -> (a -> a) -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> (a -> a) -> m ()
modifyRef Ref m a
Ref (InferT s m) a
x ((a -> a) -> m ()) -> (a -> a) -> m ()
forall a b. (a -> b) -> a -> b
$ (a, b) -> a
forall a b. (a, b) -> a
fst ((a, b) -> a) -> (a -> (a, b)) -> a -> a
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 :: e -> InferT s m a
throwM = InferError -> InferT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InferError -> InferT s m a)
-> (e -> InferError) -> e -> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> InferError
forall s. Exception s => s -> InferError
EvaluationError

instance Monad m => MonadCatch (InferT s m) where
  catch :: 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 =
    InferT s m a -> (InferError -> InferT s m a) -> InferT s m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError InferT s m a
m ((InferError -> InferT s m a) -> InferT s m a)
-> (InferError -> InferT s m a) -> InferT s m a
forall a b. (a -> b) -> a -> b
$
      \case
        EvaluationError s
e ->
          InferT s m a -> (e -> InferT s m a) -> Maybe e -> InferT s m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
            (Text -> InferT s m a
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> InferT s m a) -> Text -> InferT s m a
forall a b. (a -> b) -> a -> b
$ Text
"Exception was not an exception: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> s -> Text
forall b a. (Show a, IsString b) => a -> b
show s
e)
            e -> InferT s m a
h
            (SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
fromException (SomeException -> Maybe e) -> SomeException -> Maybe e
forall a b. (a -> b) -> a -> b
$ s -> SomeException
forall e. Exception e => e -> SomeException
toException s
e)
        InferError
err -> Text -> InferT s m a
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> InferT s m a) -> Text -> InferT s m a
forall a b. (a -> b) -> a -> b
$ Text
"Unexpected error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> InferError -> Text
forall b a. (Show a, IsString b) => a -> b
show InferError
err

-- instance MonadThunkId m => MonadThunkId (InferT s m) where
--   type ThunkId (InferT s m) = ThunkId m

instance
  Monad m
  => FromValue NixString (InferT s m) (Judgment s)
 where
  fromValueMay :: Judgment s -> InferT s m (Maybe NixString)
fromValueMay Judgment s
_ = InferT s m (Maybe NixString)
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
  fromValue :: Judgment s -> InferT s m NixString
fromValue Judgment s
_ = Text -> InferT s m NixString
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 = (Type -> Judgment s) -> b -> Type -> Judgment s
forall a b. a -> b -> a
const Type -> Judgment s
forall s. Type -> Judgment s
inferred
      Maybe (AttrSet (Judgment s), PositionSet)
-> InferT s m (Maybe (AttrSet (Judgment s), PositionSet))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (AttrSet (Judgment s), PositionSet)
 -> InferT s m (Maybe (AttrSet (Judgment s), PositionSet)))
-> Maybe (AttrSet (Judgment s), PositionSet)
-> InferT s m (Maybe (AttrSet (Judgment s), PositionSet))
forall a b. (a -> b) -> a -> b
$ (AttrSet (Judgment s), PositionSet)
-> Maybe (AttrSet (Judgment s), PositionSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((VarName -> Type -> Judgment s)
-> AttrSet Type -> AttrSet (Judgment s)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey VarName -> Type -> Judgment s
forall b s. b -> Type -> Judgment s
sing AttrSet Type
xs, PositionSet
forall a. Monoid a => a
mempty)
  fromValueMay Judgment s
_ = InferT s m (Maybe (AttrSet (Judgment s), PositionSet))
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
  fromValue :: Judgment s -> InferT s m (AttrSet (Judgment s), PositionSet)
fromValue =
    (AttrSet (Judgment s), PositionSet)
-> InferT s m (AttrSet (Judgment s), PositionSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((AttrSet (Judgment s), PositionSet)
 -> InferT s m (AttrSet (Judgment s), PositionSet))
-> (Maybe (AttrSet (Judgment s), PositionSet)
    -> (AttrSet (Judgment s), PositionSet))
-> Maybe (AttrSet (Judgment s), PositionSet)
-> InferT s m (AttrSet (Judgment s), PositionSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Maybe (AttrSet (Judgment s), PositionSet)
-> (AttrSet (Judgment s), PositionSet)
forall m. Monoid m => Maybe m -> m
maybeToMonoid
      (Maybe (AttrSet (Judgment s), PositionSet)
 -> InferT s m (AttrSet (Judgment s), PositionSet))
-> (Judgment s
    -> InferT s m (Maybe (AttrSet (Judgment s), PositionSet)))
-> Judgment s
-> InferT s m (AttrSet (Judgment s), PositionSet)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Judgment s
-> InferT s m (Maybe (AttrSet (Judgment s), PositionSet))
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 :: (t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith t c -> c
fld b -> c
getter a -> f b
init =
  -- maybe here is some law?
  (t c -> c) -> f (t c) -> f c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t c -> c
fld (f (t c) -> f c) -> (t a -> f (t c)) -> t a -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f c) -> t a -> f (t c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((b -> c) -> f b -> f c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
getter (f b -> f c) -> (a -> f b) -> a -> f c
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 :: (t Type -> Type) -> t (Judgment s) -> InferT s m (Judgment s)
toJudgment t Type -> Type
c t (Judgment s)
xs =
  (Assumption -> [Constraint] -> Type -> Judgment s)
-> InferT s m Assumption
-> InferT s m [Constraint]
-> InferT s m Type
-> InferT s m (Judgment s)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
    ((t Assumption -> Assumption)
-> (Judgment s -> Assumption) -> InferT s m Assumption
forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t Assumption -> Assumption
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Judgment s -> Assumption
forall s. Judgment s -> Assumption
assumptions    )
    ((t [Constraint] -> [Constraint])
-> (Judgment s -> [Constraint]) -> InferT s m [Constraint]
forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t [Constraint] -> [Constraint]
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Judgment s -> [Constraint]
forall s. Judgment s -> [Constraint]
typeConstraints)
    ((t Type -> Type) -> (Judgment s -> Type) -> InferT s m Type
forall a. (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t Type -> Type
c    Judgment s -> Type
forall s. Judgment s -> Type
inferredType   )
   where
    foldWith :: (t a -> a) -> (Judgment s -> a) -> InferT s m a
    foldWith :: (t a -> a) -> (Judgment s -> a) -> InferT s m a
foldWith t a -> a
g Judgment s -> a
f = (t a -> a)
-> (Judgment s -> a)
-> (Judgment s -> InferT s m (Judgment s))
-> t (Judgment s)
-> InferT s m a
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 Judgment s -> InferT s m (Judgment s)
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
_) = (AttrSet Type -> Type)
-> AttrSet (Judgment s) -> InferT s m (Judgment s)
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 -- why variadic? Probably `Closed` (`mempty`)?

instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
  toValue :: [Judgment s] -> InferT s m (Judgment s)
toValue = ([Type] -> Type) -> [Judgment s] -> InferT s m (Judgment s)
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
_ = Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Type -> Judgment s
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   = InferT s m (Scopes (InferT s m) (Judgment s))
forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
m (Scopes m a)
askScopesReader
  clearScopes :: InferT s m r -> InferT s m r
clearScopes = forall e r.
(MonadReader e (InferT s m),
 Has e (Scopes (InferT s m) (Judgment s))) =>
InferT s m r -> InferT s m r
forall (m :: * -> *) a e r.
(MonadReader e m, Has e (Scopes m a)) =>
m r -> m r
clearScopesReader @(InferT s m) @(Judgment s)
  pushScopes :: Scopes (InferT s m) (Judgment s) -> InferT s m r -> InferT s m r
pushScopes  = Scopes (InferT s m) (Judgment s) -> InferT s m r -> InferT s m r
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   = VarName -> InferT s m (Maybe (Judgment s))
forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
VarName -> m (Maybe a)
lookupVarReader

-- newtype JThunkT s m = JThunk (NThunkF (InferT s m) (Judgment s))

--  2021-02-22: NOTE: Seems like suporflous instance
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  = InferT s m (Judgment s) -> InferT s m (Judgment s)
forall a. a -> a
id

  demand
    :: Judgment s
    -> InferT s m (Judgment s)
  demand :: Judgment s -> InferT s m (Judgment s)
demand = Judgment s -> InferT s m (Judgment s)
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 = Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure


--  2021-02-22: NOTE: Seems like suporflous instance
instance Monad m => MonadValueF (Judgment s) (InferT s m) where

  demandF
    :: ( Judgment s
      -> InferT s m r)
    -> Judgment s
    -> InferT s m r
  demandF :: (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 (InferT s m (Judgment s) -> InferT s m (Judgment s))
-> (Judgment s -> InferT s m (Judgment s))
-> Judgment s
-> InferT s m (Judgment s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

{-
instance MonadInfer m
  => MonadThunk (JThunkT s m) (InferT s m) (Judgment s) where

  thunkId (JThunk x) = thunkId x

  thunk = fmap JThunk . thunk

  query b (JThunk x) = query b x

  -- If we have a thunk loop, we just don't know the type.
  force (JThunk t) = catch (force t)
    $ \(_ :: ThunkLoop) ->
                           f =<< Judgment mempty mempty <$> fresh

  -- If we have a thunk loop, we just don't know the type.
  forceEff (JThunk t) = catch (forceEff t)
    $ \(_ :: ThunkLoop) ->
                           f =<< Judgment mempty mempty <$> fresh
-}

polymorphicVar :: MonadInfer m => VarName -> InferT s m (Judgment s)
polymorphicVar :: VarName -> InferT s m (Judgment s)
polymorphicVar VarName
var =
  (Type -> Judgment s) -> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
    ((Type -> Type -> Judgment s) -> Type -> Judgment s
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((Type -> Type -> Judgment s) -> Type -> Judgment s)
-> (Type -> Type -> Judgment s) -> Type -> Judgment s
forall a b. (a -> b) -> a -> b
$ (Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
`Judgment` [Constraint]
forall a. Monoid a => a
mempty) (Assumption -> Type -> Judgment s)
-> (Type -> Assumption) -> Type -> Type -> Judgment s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VarName, Type) -> Assumption) -> VarName -> Type -> Assumption
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (VarName, Type) -> Assumption
forall x. One x => OneItem x -> x
one VarName
var)
    InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh

constInfer :: Applicative f => Type -> b -> f (Judgment s)
constInfer :: Type -> b -> f (Judgment s)
constInfer Type
x = f (Judgment s) -> b -> f (Judgment s)
forall a b. a -> b -> a
const (f (Judgment s) -> b -> f (Judgment s))
-> f (Judgment s) -> b -> f (Judgment s)
forall a b. (a -> b) -> a -> b
$ Judgment s -> f (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> f (Judgment s)) -> Judgment s -> f (Judgment s)
forall a b. (a -> b) -> a -> b
$ Type -> Judgment s
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 = VarName -> InferT s m (Judgment s)
forall (m :: * -> *) s.
MonadInfer m =>
VarName -> InferT s m (Judgment s)
polymorphicVar

  synHole :: VarName -> InferT s m (Judgment s)
synHole = VarName -> InferT s m (Judgment s)
forall (m :: * -> *) s.
MonadInfer m =>
VarName -> InferT s m (Judgment s)
polymorphicVar

  -- If we fail to look up an attribute, we just don't know the type.
  attrMissing :: NonEmpty VarName -> Maybe (Judgment s) -> InferT s m (Judgment s)
attrMissing NonEmpty VarName
_ Maybe (Judgment s)
_ = Type -> Judgment s
forall s. Type -> Judgment s
inferred (Type -> Judgment s) -> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh

  evaledSym :: VarName -> Judgment s -> InferT s m (Judgment s)
evaledSym VarName
_ = Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

  evalCurPos :: InferT s m (Judgment s)
evalCurPos =
    Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$
      Type -> Judgment s
forall s. Type -> Judgment s
inferred (Type -> Judgment s) -> Type -> Judgment s
forall a b. (a -> b) -> a -> b
$
        Variadic -> AttrSet Type -> Type
TSet Variadic
forall a. Monoid a => a
mempty (AttrSet Type -> Type) -> AttrSet Type -> Type
forall a b. (a -> b) -> a -> b
$
          [(VarName, Type)] -> AttrSet Type
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 = Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Type -> Judgment s
forall s. Type -> Judgment s
inferred (Type -> Judgment s) -> Type -> Judgment s
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      = Type
-> NString (InferT s m (Judgment s)) -> InferT s m (Judgment s)
forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
typeString
  evalLiteralPath :: Path -> InferT s m (Judgment s)
evalLiteralPath = Type -> Path -> InferT s m (Judgment s)
forall (f :: * -> *) b s.
Applicative f =>
Type -> b -> f (Judgment s)
constInfer Type
typePath
  evalEnvPath :: Path -> InferT s m (Judgment s)
evalEnvPath     = Type -> Path -> InferT s m (Judgment s)
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) =
    (Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
as1 ([Constraint] -> Type -> Judgment s)
-> (Type -> [Constraint]) -> Type -> Judgment s
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<>) ([Constraint] -> [Constraint])
-> (Type -> [Constraint]) -> Type -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> NUnaryOp -> [Constraint]
`unops` NUnaryOp
op) (Type -> [Constraint]) -> (Type -> Type) -> Type -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type
t1 Type -> Type -> Type
:~>)) (Type -> Judgment s) -> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferT s m Type
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
      (Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment (Assumption
as1 Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
as2) ([Constraint] -> Type -> Judgment s)
-> (Type -> [Constraint]) -> Type -> Judgment s
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2) [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<>) ([Constraint] -> [Constraint])
-> (Type -> [Constraint]) -> Type -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> NBinaryOp -> [Constraint]
`binops` NBinaryOp
op) (Type -> [Constraint]) -> (Type -> Type) -> Type -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Type
t1 Type -> Type -> Type
:~> Type
t2) Type -> Type -> Type
:~>)) (Type -> Judgment s) -> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferT s m Type
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 = InferT s m (Judgment s)
-> InferT s m (Judgment s) -> InferT s m (Judgment s)
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
    Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$
      Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
        (Assumption
as1 Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
as2 Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
as3)
        ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs3 [Constraint] -> [Constraint] -> [Constraint]
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
    Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$
      Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
        (Assumption
as1 Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
as2)
        ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> OneItem [Constraint] -> [Constraint]
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                  <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
    pure $
      Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
        (Assumption
as1 Assumption -> Assumption -> Assumption
forall a. Semigroup a => a -> a -> a
<> Assumption
as2)
        ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> OneItem [Constraint] -> [Constraint]
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 <- InferT s m TVar
forall (m :: * -> *). MonadState InferState m => m TVar
freshTVar
    let tv :: Type
tv = TVar -> Type
TVar TVar
a
    ((), Judgment Assumption
as [Constraint]
cs Type
t) <-
      TVar -> InferT s m ((), Judgment s) -> InferT s m ((), Judgment s)
forall s (m :: * -> *) a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet
        TVar
a
        (InferT s m ((), Judgment s) -> InferT s m ((), Judgment s))
-> InferT s m ((), Judgment s) -> InferT s m ((), Judgment s)
forall a b. (a -> b) -> a -> b
$ InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
    -> InferT s m (Judgment s) -> InferT s m ((), Judgment s))
-> 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)
k
          (Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type -> Type -> Judgment s) -> Type -> Judgment s
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
`Judgment` [Constraint]
forall a. Monoid a => a
mempty) (Assumption -> Type -> Judgment s)
-> (Type -> Assumption) -> Type -> Type -> Judgment s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VarName, Type) -> Assumption) -> VarName -> Type -> Assumption
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (VarName, Type) -> Assumption
forall x. One x => OneItem x -> x
one VarName
x ) Type
tv))
          ((AttrSet (InferT s m (Judgment s))
  -> InferT s m (Judgment s) -> InferT s m ((), Judgment s))
 -> InferT s m ((), Judgment s))
-> (AttrSet (InferT s m (Judgment s))
    -> InferT s m (Judgment s) -> InferT s m ((), Judgment s))
-> InferT s m ((), Judgment s)
forall a b. (a -> b) -> a -> b
$ (InferT s m (Judgment s) -> InferT s m ((), Judgment s))
-> AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s)
-> InferT s m ((), Judgment s)
forall a b. a -> b -> a
const ((InferT s m (Judgment s) -> InferT s m ((), Judgment s))
 -> AttrSet (InferT s m (Judgment s))
 -> InferT s m (Judgment s)
 -> InferT s m ((), Judgment s))
-> (InferT s m (Judgment s) -> InferT s m ((), Judgment s))
-> AttrSet (InferT s m (Judgment s))
-> InferT s m (Judgment s)
-> InferT s m ((), Judgment s)
forall a b. (a -> b) -> a -> b
$ (Judgment s -> ((), Judgment s))
-> InferT s m (Judgment s) -> InferT s m ((), Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (()
forall a. Monoid a => a
mempty,)
    Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$
      Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
        (Assumption
as Assumption -> VarName -> Assumption
`Assumption.remove` VarName
x)
        ([Constraint]
cs [Constraint] -> [Constraint] -> [Constraint]
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 <- ([[(VarName, Type)]] -> [(VarName, Type)])
-> ((VarName, Type) -> [(VarName, Type)])
-> ((VarName, Maybe (InferT s m (Judgment s)))
    -> InferT s m (VarName, Type))
-> ParamSet (InferT s m (Judgment s))
-> InferT s m [(VarName, Type)]
forall (t :: * -> *) (f :: * -> *) c b a.
(Traversable t, Applicative f) =>
(t c -> c) -> (b -> c) -> (a -> f b) -> t a -> f c
foldInitializedWith [[(VarName, Type)]] -> [(VarName, Type)]
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (VarName, Type) -> [(VarName, Type)]
forall x. One x => OneItem x -> x
one (VarName, Maybe (InferT s m (Judgment s)))
-> InferT s m (VarName, Type)
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 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> OneItem a -> a
forall x. One x => OneItem x -> x
one (k
k, v
t), k -> v -> HashMap k v -> HashMap k v
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) = ((Assumption, AttrSet Type)
 -> (VarName, Type) -> (Assumption, AttrSet Type))
-> (Assumption, AttrSet Type)
-> [(VarName, Type)]
-> (Assumption, AttrSet Type)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Assumption, AttrSet Type)
-> (VarName, Type) -> (Assumption, AttrSet Type)
forall a k v.
(Semigroup a, One a, Eq k, Hashable k, OneItem a ~ (k, v)) =>
(a, HashMap k v) -> (k, v) -> (a, HashMap k v)
f (Assumption, AttrSet Type)
forall a. Monoid a => a
mempty [(VarName, Type)]
js
      arg :: InferT s m (Judgment s)
arg   = Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Judgment s -> InferT s m (Judgment s))
-> Judgment s -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
env [Constraint]
forall a. Monoid a => a
mempty (Type -> Judgment s) -> Type -> Judgment s
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  = InferT s m (Judgment s)
-> (AttrSet (InferT s m (Judgment s))
    -> InferT s m (Judgment s)
    -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
-> InferT s m (AttrSet (InferT s m (Judgment s)), 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)
k InferT s m (Judgment s)
arg ((AttrSet (InferT s m (Judgment s))
  -> InferT s m (Judgment s)
  -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
 -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
-> (AttrSet (InferT s m (Judgment s))
    -> InferT s m (Judgment s)
    -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
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, ) (Judgment s -> (AttrSet (InferT s m (Judgment s)), Judgment s))
-> InferT s m (Judgment s)
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferT s m (Judgment s)
b
      names :: [VarName]
names = (VarName, Type) -> VarName
forall a b. (a, b) -> a
fst ((VarName, Type) -> VarName) -> [(VarName, Type)] -> [VarName]
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) <- ((VarName, Type)
 -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
 -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
-> [(VarName, Type)]
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TVar
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
forall s (m :: * -> *) a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet (TVar
 -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
 -> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s))
-> ((VarName, Type) -> TVar)
-> (VarName, Type)
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (TVar TVar
a) -> TVar
a) (Type -> TVar)
-> ((VarName, Type) -> Type) -> (VarName, Type) -> TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarName, Type) -> Type
forall a b. (a, b) -> b
snd) InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
call [(VarName, Type)]
js

    Type
ty <- (AttrSet Type -> Type)
-> (Judgment s -> Type)
-> (InferT s m (Judgment s) -> InferT s m (Judgment s))
-> AttrSet (InferT s m (Judgment s))
-> InferT s m Type
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) Judgment s -> Type
forall s. Judgment s -> Type
inferredType InferT s m (Judgment s) -> InferT s m (Judgment s)
forall a. a -> a
id AttrSet (InferT s m (Judgment s))
args

    pure $
      Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
        ((Assumption -> VarName -> Assumption)
-> Assumption -> [VarName] -> Assumption
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 [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [ Type -> Type -> Constraint
EqConst Type
t' (AttrSet Type
tys AttrSet Type -> VarName -> Type
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 :: s -> InferT s m a
evalError = InferError -> InferT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InferError -> InferT s m a)
-> (s -> InferError) -> s -> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> InferError
forall s. Exception s => s -> InferError
EvaluationError

-- * class @FreeTypeVars@

class FreeTypeVars a where
  ftv :: a -> Set.Set TVar

occursCheck :: FreeTypeVars a => TVar -> a -> Bool
occursCheck :: TVar -> a -> Bool
occursCheck TVar
a a
t = TVar
a TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` a -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv a
t

-- ** Instances

instance FreeTypeVars Type where
  ftv :: Type -> Set TVar
ftv TCon{}      = Set TVar
forall a. Monoid a => a
mempty
  ftv (TVar TVar
a   ) = OneItem (Set TVar) -> Set TVar
forall x. One x => OneItem x -> x
one OneItem (Set TVar)
TVar
a
  ftv (TSet Variadic
_ AttrSet Type
a ) = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv (Type -> Set TVar) -> [Type] -> [Set TVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrSet Type -> [Type]
forall k v. HashMap k v -> [v]
M.elems AttrSet Type
a
  ftv (TList [Type]
a  ) = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv (Type -> Set TVar) -> [Type] -> [Set TVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
a
  ftv (Type
t1 :~> Type
t2) = Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
<> Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2
  ftv (TMany [Type]
ts ) = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv (Type -> Set TVar) -> [Type] -> [Set TVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts

instance FreeTypeVars TVar where
  ftv :: TVar -> Set TVar
ftv = TVar -> Set TVar
forall x. One x => OneItem x -> x
one

instance FreeTypeVars Scheme where
  ftv :: Scheme -> Set TVar
ftv (Forall [TVar]
as Type
t) = Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList [TVar]
as

instance FreeTypeVars a => FreeTypeVars [a] where
  ftv :: [a] -> Set TVar
ftv = (a -> Set TVar -> Set TVar) -> Set TVar -> [a] -> Set TVar
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
(<>) (Set TVar -> Set TVar -> Set TVar)
-> (a -> Set TVar) -> a -> Set TVar -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv) Set TVar
forall a. Monoid a => a
mempty

instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
  ftv :: Set a -> Set TVar
ftv = (a -> Set TVar -> Set TVar) -> Set TVar -> Set a -> Set TVar
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
(<>) (Set TVar -> Set TVar -> Set TVar)
-> (a -> Set TVar) -> a -> Set TVar -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv) Set TVar
forall a. Monoid a => a
mempty

-- * class @ActiveTypeVars@

class ActiveTypeVars a where
  atv :: a -> Set.Set TVar

-- ** Instances

instance ActiveTypeVars Constraint where
  atv :: Constraint -> Set TVar
atv (EqConst      Type
t1 Type
t2   ) = Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
<> Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2
  atv (ImpInstConst Type
t1 Set TVar
ms Type
t2) = Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t1 Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
<> (Set TVar -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Set TVar
ms Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2)
  atv (ExpInstConst Type
t  Scheme
s    ) = Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t  Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
<> Scheme -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Scheme
s

instance ActiveTypeVars a => ActiveTypeVars [a] where
  atv :: [a] -> Set TVar
atv = (a -> Set TVar -> Set TVar) -> Set TVar -> [a] -> Set TVar
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set TVar -> Set TVar -> Set TVar
forall a. Semigroup a => a -> a -> a
(<>) (Set TVar -> Set TVar -> Set TVar)
-> (a -> Set TVar) -> a -> Set TVar -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set TVar
forall a. ActiveTypeVars a => a -> Set TVar
atv) Set TVar
forall a. Monoid a => a
mempty

-- * Other

type MonadInfer m
  = ({- MonadThunkId m,-}
     MonadAtomicRef m, MonadFix m)

-- | Run the inference monad
runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
runInfer' :: InferT s m a -> m (Either InferError a)
runInfer' =
  ExceptT InferError m a -> m (Either InferError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
    (ExceptT InferError m a -> m (Either InferError a))
-> (InferT s m a -> ExceptT InferError m a)
-> InferT s m a
-> m (Either InferError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT InferState (ExceptT InferError m) a
-> InferState -> ExceptT InferError m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` InferState
initInfer)
    (StateT InferState (ExceptT InferError m) a
 -> ExceptT InferError m a)
-> (InferT s m a -> StateT InferState (ExceptT InferError m) a)
-> InferT s m a
-> ExceptT InferError m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> (Set TVar, Scopes (InferT s m) (Judgment s))
-> StateT InferState (ExceptT InferError m) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Set TVar, Scopes (InferT s m) (Judgment s))
forall a. Monoid a => a
mempty)
    (ReaderT
   (Set TVar, Scopes (InferT s m) (Judgment s))
   (StateT InferState (ExceptT InferError m))
   a
 -> StateT InferState (ExceptT InferError m) a)
-> (InferT s m a
    -> ReaderT
         (Set TVar, Scopes (InferT s m) (Judgment s))
         (StateT InferState (ExceptT InferError m))
         a)
-> InferT s m a
-> StateT InferState (ExceptT InferError m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InferT s m a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
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 s. InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer forall s. InferT s (FreshIdT Int (ST s)) a
m =
  (forall s. ST s (Either InferError a)) -> Either InferError a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Either InferError a)) -> Either InferError a)
-> (forall s. ST s (Either InferError a)) -> Either InferError a
forall a b. (a -> b) -> a -> b
$ FreshIdT Int (ST s) (Either InferError a)
-> Ref (ST s) Int -> ST s (Either InferError a)
forall (m :: * -> *) i a.
Functor m =>
FreshIdT i m a -> Ref m i -> m a
runFreshIdT (InferT s (FreshIdT Int (ST s)) a
-> FreshIdT Int (ST s) (Either InferError a)
forall (m :: * -> *) s a.
MonadInfer m =>
InferT s m a -> m (Either InferError a)
runInfer' InferT s (FreshIdT Int (ST s)) a
forall s. InferT s (FreshIdT Int (ST s)) a
m) (STRef s Int -> ST s (Either InferError a))
-> ST s (STRef s Int) -> ST s (Either InferError a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> ST s (Ref (ST s) Int)
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 :: Env -> NExpr -> InferT s m [(Subst, Type)]
inferType Env
env NExpr
ex =
  do
    Judgment Assumption
as [Constraint]
cs Type
t <- NExpr -> InferT s m (Judgment s)
forall (m :: * -> *) s.
MonadInfer m =>
NExpr -> InferT s m (Judgment s)
infer NExpr
ex
    let
      unbounds :: Set VarName
      unbounds :: Set VarName
unbounds =
        (Set VarName -> Set VarName -> Set VarName
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set VarName -> Set VarName -> Set VarName)
-> ([VarName] -> Set VarName)
-> [VarName]
-> [VarName]
-> Set VarName
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [VarName] -> Set VarName
forall a. Ord a => [a] -> Set a
Set.fromList)
          (Assumption -> [VarName]
Assumption.keys Assumption
as )
          (       Env -> [VarName]
Env.keys Env
env)
    Bool -> InferT s m () -> InferT s m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
      (Set VarName -> Bool
forall a. Set a -> Bool
Set.null Set VarName
unbounds)
      (InferT s m () -> InferT s m ()) -> InferT s m () -> InferT s m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> InferT s m ()
forall (m :: * -> *). MonadError InferError m => TypeError -> m ()
typeError (TypeError -> InferT s m ()) -> TypeError -> InferT s m ()
forall a b. (a -> b) -> a -> b
$ [VarName] -> TypeError
UnboundVariables ([VarName] -> TypeError) -> [VarName] -> TypeError
forall a b. (a -> b) -> a -> b
$ [VarName] -> [VarName]
forall a. Ord a => [a] -> [a]
ordNub ([VarName] -> [VarName]) -> [VarName] -> [VarName]
forall a b. (a -> b) -> a -> b
$ Set VarName -> [VarName]
forall a. Set a -> [a]
Set.toList Set VarName
unbounds

    InferState
inferState <- InferT s m 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 =
        (State InferState (Either [TypeError] [(Subst, Type)])
-> InferState -> Either [TypeError] [(Subst, Type)]
forall s a. State s a -> s -> a
`evalState` InferState
inferState) (State InferState (Either [TypeError] [(Subst, Type)])
 -> Either [TypeError] [(Subst, Type)])
-> (Solver (StateT InferState Identity) (Subst, Type)
    -> State InferState (Either [TypeError] [(Subst, Type)]))
-> Solver (StateT InferState Identity) (Subst, Type)
-> Either [TypeError] [(Subst, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solver (StateT InferState Identity) (Subst, Type)
-> State InferState (Either [TypeError] [(Subst, Type)])
forall (m :: * -> *) a.
Monad m =>
Solver m a -> m (Either [TypeError] [a])
runSolver (Solver (StateT InferState Identity) (Subst, Type)
 -> Either [TypeError] [(Subst, Type)])
-> Solver (StateT InferState Identity) (Subst, Type)
-> Either [TypeError] [(Subst, Type)]
forall a b. (a -> b) -> a -> b
$ (Subst -> Type) -> (Subst, Subst) -> (Subst, Type)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
`apply` Type
t) ((Subst, Subst) -> (Subst, Type))
-> (Subst -> (Subst, Subst)) -> Subst -> (Subst, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Subst -> Subst -> (Subst, Subst)) -> Subst -> (Subst, Subst)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (,) (Subst -> (Subst, Type))
-> Solver (StateT InferState Identity) Subst
-> Solver (StateT InferState Identity) (Subst, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint] -> Solver (StateT InferState Identity) Subst
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve ([Constraint]
cs [Constraint] -> [Constraint] -> [Constraint]
forall a. Semigroup a => a -> a -> a
<> [Constraint]
cs')

    ([TypeError] -> InferT s m [(Subst, Type)])
-> ([(Subst, Type)] -> InferT s m [(Subst, Type)])
-> Either [TypeError] [(Subst, Type)]
-> InferT s m [(Subst, Type)]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
      (InferError -> InferT s m [(Subst, Type)]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InferError -> InferT s m [(Subst, Type)])
-> ([TypeError] -> InferError)
-> [TypeError]
-> InferT s m [(Subst, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeError] -> InferError
TypeInferenceErrors)
      [(Subst, Type)] -> InferT s m [(Subst, Type)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      Either [TypeError] [(Subst, Type)]
evalResult

-- | Solve for the toplevel type of an expression in a given environment
inferExpr :: Env -> NExpr -> Either InferError [Scheme]
inferExpr :: Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex =
  Type -> Scheme
closeOver (Type -> Scheme)
-> ((Subst, Type) -> Type) -> (Subst, Type) -> Scheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Subst -> Type -> Type) -> (Subst, Type) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply ((Subst, Type) -> Scheme)
-> Either InferError [(Subst, Type)] -> Either InferError [Scheme]
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> f (g a) -> f (g b)
<<$>> (forall s. InferT s (FreshIdT Int (ST s)) [(Subst, Type)])
-> Either InferError [(Subst, Type)]
forall a.
(forall s. InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer (Env -> NExpr -> InferT s (FreshIdT Int (ST s)) [(Subst, Type)]
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 =
  OneItem [Constraint] -> [Constraint]
forall x. One x => OneItem x -> x
one (OneItem [Constraint] -> [Constraint])
-> OneItem [Constraint] -> [Constraint]
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> Constraint
EqConst Type
u1 (Type -> Constraint) -> Type -> Constraint
forall a b. (a -> b) -> a -> b
$
      case NUnaryOp
op of
        NUnaryOp
NNot -> Type -> Type
mkUnaryConstr Type
typeBool
        NUnaryOp
NNeg -> [Type] -> Type
TMany ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkUnaryConstr (Type -> Type) -> [Type] -> [Type]
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 (NonEmpty Type -> Type) -> (Type -> NonEmpty Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk2same
   where
    mk2same :: a -> NonEmpty a
    mk2same :: a -> NonEmpty a
mk2same a
a = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| OneItem [a] -> [a]
forall x. One x => OneItem x -> x
one a
OneItem [a]
a

binops :: Type -> NBinaryOp -> [Constraint]
binops :: Type -> NBinaryOp -> [Constraint]
binops Type
u1 NBinaryOp
op =
  if
    -- NApp in fact is handled separately
    -- Equality tells nothing about the types, because any two types are allowed.
    | NBinaryOp
op NBinaryOp -> [NBinaryOp] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NApp  , NBinaryOp
NEq  , NBinaryOp
NNEq        ] -> [Constraint]
forall a. Monoid a => a
mempty
    | NBinaryOp
op NBinaryOp -> [NBinaryOp] -> Bool
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 NBinaryOp -> [NBinaryOp] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NAnd  , NBinaryOp
NOr  , NBinaryOp
NImpl       ] -> [Constraint]
gate
    | NBinaryOp
op NBinaryOp -> NBinaryOp -> Bool
forall a. Eq a => a -> a -> Bool
==       NBinaryOp
NConcat                      -> [Constraint]
concatenation
    | NBinaryOp
op NBinaryOp -> [NBinaryOp] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ NBinaryOp
NMinus, NBinaryOp
NMult, NBinaryOp
NDiv        ] -> [Constraint]
arithmetic
    | NBinaryOp
op NBinaryOp -> NBinaryOp -> Bool
forall a. Eq a => a -> a -> Bool
==       NBinaryOp
NUpdate                      -> [Constraint]
rUnion
    | NBinaryOp
op NBinaryOp -> NBinaryOp -> Bool
forall a. Eq a => a -> a -> Bool
==       NBinaryOp
NPlus                        -> [Constraint]
addition
    | Bool
otherwise -> String -> [Constraint]
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 :: a -> a -> a -> NonEmpty a
mk3 a
a a
b a
c = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a
b, a
c]

  mk3same :: a -> NonEmpty a
  mk3same :: a -> NonEmpty a
mk3same a
a = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a
a, a
a]

  allConst :: Type -> [Constraint]
  allConst :: Type -> [Constraint]
allConst = Constraint -> [Constraint]
forall x. One x => OneItem x -> x
one (Constraint -> [Constraint])
-> (Type -> Constraint) -> Type -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Constraint
EqConst Type
u1 (Type -> Constraint) -> (Type -> Type) -> Type -> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Type -> Type
typeFun (NonEmpty Type -> Type) -> (Type -> NonEmpty Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> NonEmpty Type
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 = Constraint -> [Constraint]
forall x. One x => OneItem x -> x
one (Constraint -> [Constraint])
-> ([NonEmpty Type] -> Constraint)
-> [NonEmpty Type]
-> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Constraint
EqConst Type
u1 (Type -> Constraint)
-> ([NonEmpty Type] -> Type) -> [NonEmpty Type] -> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
TMany ([Type] -> Type)
-> ([NonEmpty Type] -> [Type]) -> [NonEmpty Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty Type -> Type) -> [NonEmpty Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty Type -> Type
typeFun

  inequality :: [Constraint]
inequality =
    [NonEmpty Type] -> [Constraint]
eqConstrMtx
      [ Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt   Type
typeInt   Type
typeBool
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeFloat Type
typeBool
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt   Type
typeFloat Type
typeBool
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeInt   Type
typeBool
      ]

  arithmetic :: [Constraint]
arithmetic =
    [NonEmpty Type] -> [Constraint]
eqConstrMtx
      [ Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeInt
      , Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeFloat
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt   Type
typeFloat Type
typeFloat
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat Type
typeInt   Type
typeFloat
      ]

  rUnion :: [Constraint]
rUnion =
    [NonEmpty Type] -> [Constraint]
eqConstrMtx
      [ Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeSet
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeSet  Type
typeNull Type
typeSet
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeNull Type
typeSet  Type
typeSet
      ]

  addition :: [Constraint]
addition =
    [NonEmpty Type] -> [Constraint]
eqConstrMtx
      [ Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeInt
      , Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeFloat
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeInt    Type
typeFloat  Type
typeFloat
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeFloat  Type
typeInt    Type
typeFloat
      , Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typeString
      , Type -> NonEmpty Type
forall a. a -> NonEmpty a
mk3same Type
typePath
      , Type -> Type -> Type -> NonEmpty Type
forall a. a -> a -> a -> NonEmpty a
mk3 Type
typeString Type
typeString Type
typePath
      ]

liftInfer :: Monad m => m a -> InferT s m a
liftInfer :: m a -> InferT s m a
liftInfer = InferTInternals s m a -> InferT s m a
forall s (m :: * -> *) a. InferTInternals s m a -> InferT s m a
InferT (InferTInternals s m a -> InferT s m a)
-> (m a -> InferTInternals s m a) -> m a -> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT InferState (ExceptT InferError m) a -> InferTInternals s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT InferState (ExceptT InferError m) a
 -> InferTInternals s m a)
-> (m a -> StateT InferState (ExceptT InferError m) a)
-> m a
-> InferTInternals s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT InferError m a
-> StateT InferState (ExceptT InferError m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT InferError m a
 -> StateT InferState (ExceptT InferError m) a)
-> (m a -> ExceptT InferError m a)
-> m a
-> StateT InferState (ExceptT InferError m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> ExceptT InferError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

-- * Other

infer :: MonadInfer m => NExpr -> InferT s m (Judgment s)
infer :: NExpr -> InferT s m (Judgment s)
infer = (NExprF (InferT s m (Judgment s)) -> InferT s m (Judgment s))
-> NExpr -> InferT s m (Judgment s)
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix NExprF (InferT s m (Judgment s)) -> InferT s m (Judgment s)
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 []                = Env -> Either InferError 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)
    ([Scheme] -> Either InferError Env)
-> Either InferError [Scheme] -> Either InferError Env
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex

-- * Other

newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a)
    deriving (a -> Solver m b -> Solver m a
(a -> b) -> Solver m a -> Solver m b
(forall a b. (a -> b) -> Solver m a -> Solver m b)
-> (forall a b. a -> Solver m b -> Solver m a)
-> Functor (Solver m)
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
<$ :: a -> Solver m b -> Solver m a
$c<$ :: forall (m :: * -> *) a b. a -> Solver m b -> Solver m a
fmap :: (a -> b) -> Solver m a -> Solver m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> Solver m a -> Solver m b
Functor, Functor (Solver m)
a -> Solver m a
Functor (Solver m)
-> (forall a. a -> Solver m a)
-> (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 a b. Solver m a -> Solver m b -> Solver m b)
-> (forall a b. Solver m a -> Solver m b -> Solver m a)
-> Applicative (Solver m)
Solver m a -> Solver m b -> Solver m b
Solver m a -> Solver m b -> Solver m a
Solver m (a -> b) -> Solver m a -> Solver m b
(a -> b -> c) -> Solver m a -> Solver m b -> Solver m c
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
<* :: Solver m a -> Solver m b -> Solver m a
$c<* :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m a
*> :: Solver m a -> Solver m b -> Solver m b
$c*> :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m b
liftA2 :: (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
<*> :: 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 :: a -> Solver m a
$cpure :: forall (m :: * -> *) a. a -> Solver m a
$cp1Applicative :: forall (m :: * -> *). Functor (Solver m)
Applicative, Applicative (Solver m)
Solver m a
Applicative (Solver m)
-> (forall a. Solver m a)
-> (forall a. Solver m a -> Solver m a -> Solver m a)
-> (forall a. Solver m a -> Solver m [a])
-> (forall a. Solver m a -> Solver m [a])
-> Alternative (Solver m)
Solver m a -> Solver m a -> Solver m a
Solver m a -> Solver m [a]
Solver m a -> Solver m [a]
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 :: Solver m a -> Solver m [a]
$cmany :: forall (m :: * -> *) a. Solver m a -> Solver m [a]
some :: Solver m a -> Solver m [a]
$csome :: forall (m :: * -> *) a. Solver m a -> Solver m [a]
<|> :: Solver m a -> Solver m a -> Solver m a
$c<|> :: forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
empty :: Solver m a
$cempty :: forall (m :: * -> *) a. Solver m a
$cp1Alternative :: forall (m :: * -> *). Applicative (Solver m)
Alternative, Applicative (Solver m)
a -> Solver m a
Applicative (Solver m)
-> (forall a b. Solver m a -> (a -> Solver m b) -> Solver m b)
-> (forall a b. Solver m a -> Solver m b -> Solver m b)
-> (forall a. a -> Solver m a)
-> Monad (Solver m)
Solver m a -> (a -> Solver m b) -> Solver m b
Solver m a -> Solver m b -> Solver m b
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 :: a -> Solver m a
$creturn :: forall (m :: * -> *) a. a -> Solver m a
>> :: Solver m a -> Solver m b -> Solver m b
$c>> :: forall (m :: * -> *) a b. Solver m a -> Solver m b -> Solver m 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
$cp1Monad :: forall (m :: * -> *). Applicative (Solver m)
Monad, Monad (Solver m)
Alternative (Solver m)
Solver m a
Alternative (Solver m)
-> Monad (Solver m)
-> (forall a. Solver m a)
-> (forall a. Solver m a -> Solver m a -> Solver m a)
-> MonadPlus (Solver m)
Solver m a -> Solver m a -> Solver m a
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 :: Solver m a -> Solver m a -> Solver m a
$cmplus :: forall (m :: * -> *) a. Solver m a -> Solver m a -> Solver m a
mzero :: Solver m a
$cmzero :: forall (m :: * -> *) a. Solver m a
$cp2MonadPlus :: forall (m :: * -> *). Monad (Solver m)
$cp1MonadPlus :: forall (m :: * -> *). Alternative (Solver m)
MonadPlus,
              MonadPlus (Solver m)
MonadPlus (Solver m)
-> (forall a. Solver m a -> Solver m (Maybe (a, Solver m a)))
-> (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 a. Solver m a -> Solver m a)
-> (forall a. Solver m a -> Solver m ())
-> MonadLogic (Solver m)
Solver m a -> Solver m (Maybe (a, Solver m a))
Solver m a -> Solver m a -> Solver m a
Solver m a -> (a -> Solver m b) -> Solver m b
Solver m a -> (a -> Solver m b) -> Solver m b -> Solver m b
Solver m a -> Solver m a
Solver m a -> Solver m ()
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 => MonadPlus (Solver 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
forall (m :: * -> *).
MonadPlus 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 b. m a -> (a -> m b) -> m b -> m b)
-> (forall a. m a -> m a)
-> (forall a. m a -> m ())
-> MonadLogic m
lnot :: Solver m a -> Solver m ()
$clnot :: forall (m :: * -> *) a. Monad m => Solver m a -> Solver m ()
once :: Solver m a -> Solver m a
$conce :: forall (m :: * -> *) a. Monad m => Solver m a -> Solver m a
ifte :: 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
>>- :: 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 :: 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 :: 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))
$cp1MonadLogic :: forall (m :: * -> *). Monad m => MonadPlus (Solver m)
MonadLogic, MonadState [TypeError])

runSolver :: forall m a . Monad m => Solver m a -> m (Either [TypeError] [a])
runSolver :: Solver m a -> m (Either [TypeError] [a])
runSolver (Solver LogicT (StateT [TypeError] m) a
s) =
  ([a] -> [TypeError] -> Either [TypeError] [a])
-> ([a], [TypeError]) -> Either [TypeError] [a]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [a] -> [TypeError] -> Either [TypeError] [a]
report (([a], [TypeError]) -> Either [TypeError] [a])
-> m ([a], [TypeError]) -> m (Either [TypeError] [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [TypeError] m [a] -> [TypeError] -> m ([a], [TypeError])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (LogicT (StateT [TypeError] m) a -> StateT [TypeError] m [a]
forall (m :: * -> *) a. Monad m => LogicT m a -> m [a]
observeAllT LogicT (StateT [TypeError] m) a
s) [TypeError]
forall a. Monoid a => a
mempty
 where
  report :: [a] -> [TypeError] -> Either [TypeError] [a]
  report :: [a] -> [TypeError] -> Either [TypeError] [a]
report [a]
xs [TypeError]
e =
    if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
xs
      then [TypeError] -> Either [TypeError] [a]
forall a b. a -> Either a b
Left ([TypeError] -> [TypeError]
forall a. Ord a => [a] -> [a]
ordNub [TypeError]
e)
      else [a] -> Either [TypeError] [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
xs

-- ** Instances

instance MonadTrans Solver where
  lift :: m a -> Solver m a
lift = LogicT (StateT [TypeError] m) a -> Solver m a
forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver (LogicT (StateT [TypeError] m) a -> Solver m a)
-> (m a -> LogicT (StateT [TypeError] m) a) -> m a -> Solver m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT [TypeError] m a -> LogicT (StateT [TypeError] m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT [TypeError] m a -> LogicT (StateT [TypeError] m) a)
-> (m a -> StateT [TypeError] m a)
-> m a
-> LogicT (StateT [TypeError] m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT [TypeError] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance Monad m => MonadError TypeError (Solver m) where
  throwError :: TypeError -> Solver m a
throwError TypeError
err = LogicT (StateT [TypeError] m) a -> Solver m a
forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver (LogicT (StateT [TypeError] m) a -> Solver m a)
-> LogicT (StateT [TypeError] m) a -> Solver m a
forall a b. (a -> b) -> a -> b
$ StateT [TypeError] m () -> LogicT (StateT [TypeError] m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (([TypeError] -> [TypeError]) -> StateT [TypeError] m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (TypeError
err TypeError -> [TypeError] -> [TypeError]
forall a. a -> [a] -> [a]
:)) LogicT (StateT [TypeError] m) ()
-> LogicT (StateT [TypeError] m) a
-> LogicT (StateT [TypeError] m) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> LogicT (StateT [TypeError] m) a
forall a. Monoid a => a
mempty
  catchError :: Solver m a -> (TypeError -> Solver m a) -> Solver m a
catchError Solver m a
_ TypeError -> Solver m a
_ = Text -> Solver m a
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"This is never used"

-- * Other

bind :: Monad m => TVar -> Type -> Solver m Subst
bind :: TVar -> Type -> Solver m Subst
bind TVar
a Type
t | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TVar -> Type
TVar TVar
a     = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
         | TVar -> Type -> Bool
forall a. FreeTypeVars a => TVar -> a -> Bool
occursCheck TVar
a Type
t = TypeError -> Solver m Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> Solver m Subst) -> TypeError -> Solver m Subst
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> TypeError
InfiniteType TVar
a Type
t
         | Bool
otherwise       = Subst -> Solver m Subst
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> Solver m Subst) -> Subst -> Solver m Subst
forall a b. (a -> b) -> a -> b
$ Map TVar Type -> Subst
Subst (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ OneItem (Map TVar Type) -> Map TVar Type
forall x. One x => OneItem x -> x
one (TVar
a, Type
t)

considering :: [a] -> Solver m a
considering :: [a] -> Solver m a
considering [a]
xs = LogicT (StateT [TypeError] m) a -> Solver m a
forall (m :: * -> *) a.
LogicT (StateT [TypeError] m) a -> Solver m a
Solver (LogicT (StateT [TypeError] m) a -> Solver m a)
-> LogicT (StateT [TypeError] m) a -> Solver m a
forall a b. (a -> b) -> a -> b
$ (forall r.
 (a -> StateT [TypeError] m r -> StateT [TypeError] m r)
 -> StateT [TypeError] m r -> StateT [TypeError] m r)
-> LogicT (StateT [TypeError] m) a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r.
  (a -> StateT [TypeError] m r -> StateT [TypeError] m r)
  -> StateT [TypeError] m r -> StateT [TypeError] m r)
 -> LogicT (StateT [TypeError] m) a)
-> (forall r.
    (a -> StateT [TypeError] m r -> StateT [TypeError] m r)
    -> StateT [TypeError] m r -> StateT [TypeError] m r)
-> LogicT (StateT [TypeError] m) a
forall a b. (a -> b) -> a -> b
$ \a -> StateT [TypeError] m r -> StateT [TypeError] m r
c StateT [TypeError] m r
n -> (a -> StateT [TypeError] m r -> StateT [TypeError] m r)
-> StateT [TypeError] m r -> [a] -> StateT [TypeError] m r
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 :: Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2 | Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2  = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TVar TVar
v) Type
t        = TVar
v TVar -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
`bind` Type
t
unifies Type
t        (TVar TVar
v) = TVar
v TVar -> Type -> Solver m Subst
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]
_) -> Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
x Type
y
        ([Type], [Type])
_              -> Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
  | [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ys = [Type] -> [Type] -> Solver m Subst
forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany [Type]
xs [Type]
ys
-- Putting a statement that lists of different lengths containing various types would not
-- be unified.
unifies t1 :: Type
t1@(TList [Type]
_    ) t2 :: Type
t2@(TList [Type]
_    ) = TypeError -> Solver m Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> Solver m Subst) -> TypeError -> Solver m Subst
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
_)                                 = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TSet Variadic
Closed   AttrSet Type
s) (TSet Variadic
Closed   AttrSet Type
b) | [VarName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (AttrSet Type -> [VarName]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b [VarName] -> [VarName] -> [VarName]
forall a. Eq a => [a] -> [a] -> [a]
\\ AttrSet Type -> [VarName]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s)   = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (TSet Variadic
_ AttrSet Type
a) (TSet Variadic
_ AttrSet Type
b) | (AttrSet Type -> [VarName]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
a [VarName] -> [VarName] -> [VarName]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` AttrSet Type -> [VarName]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b) [VarName] -> [VarName] -> Bool
forall a. Eq a => a -> a -> Bool
== AttrSet Type -> [VarName]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifies (Type
t1 :~> Type
t2) (Type
t3 :~> Type
t4) = [Type] -> [Type] -> Solver m Subst
forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany [Type
t1, Type
t2] [Type
t3, Type
t4]
unifies (TMany [Type]
t1s) Type
t2          = [Type] -> Solver m Type
forall a (m :: * -> *). [a] -> Solver m a
considering [Type]
t1s Solver m Type -> (Type -> Solver m Subst) -> Solver m Subst
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- (Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
`unifies` Type
t2)
unifies Type
t1          (TMany [Type]
t2s) = [Type] -> Solver m Type
forall a (m :: * -> *). [a] -> Solver m a
considering [Type]
t2s Solver m Type -> (Type -> Solver m Subst) -> Solver m Subst
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1
unifies Type
t1          Type
t2          = TypeError -> Solver m Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> Solver m Subst) -> TypeError -> Solver m Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
UnificationFail Type
t1 Type
t2

unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany :: [Type] -> [Type] -> Solver m Subst
unifyMany []         []         = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
unifyMany (Type
t1 : [Type]
ts1) (Type
t2 : [Type]
ts2) =
  do
    Subst
su1 <- Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2
    Subst
su2 <-
      ([Type] -> [Type] -> Solver m Subst
forall (m :: * -> *). Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany ([Type] -> [Type] -> Solver m Subst)
-> ([Type] -> [Type]) -> [Type] -> [Type] -> Solver m Subst
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Subst -> [Type] -> [Type]
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 = TypeError -> Solver m Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> Solver m Subst) -> TypeError -> Solver m Subst
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> TypeError
UnificationMismatch [Type]
t1 [Type]
t2

nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable = Maybe (Constraint, [Constraint]) -> (Constraint, [Constraint])
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Constraint, [Constraint]) -> (Constraint, [Constraint]))
-> ([Constraint] -> Maybe (Constraint, [Constraint]))
-> [Constraint]
-> (Constraint, [Constraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Constraint, [Constraint]) -> Bool)
-> [(Constraint, [Constraint])] -> Maybe (Constraint, [Constraint])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Constraint, [Constraint]) -> Bool
solvable ([(Constraint, [Constraint])] -> Maybe (Constraint, [Constraint]))
-> ([Constraint] -> [(Constraint, [Constraint])])
-> [Constraint]
-> Maybe (Constraint, [Constraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> [(Constraint, [Constraint])]
forall a. Eq a => [a] -> [(a, [a])]
pickFirstOne
 where
  pickFirstOne :: Eq a => [a] -> [(a, [a])]
  pickFirstOne :: [a] -> [(a, [a])]
pickFirstOne [a]
xs = [ (a
x, [a]
ys) | a
x <- [a]
xs, let ys :: [a]
ys = a -> [a] -> [a]
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) =
    Set TVar -> Bool
forall a. Set a -> Bool
Set.null (Set TVar -> Bool) -> Set TVar -> Bool
forall a b. (a -> b) -> a -> b
$ (Set TVar
ms Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv Type
t2) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` [Constraint] -> Set TVar
forall a. ActiveTypeVars a => a -> Set TVar
atv [Constraint]
cs

solve :: forall m . MonadState InferState m => [Constraint] -> Solver m Subst
solve :: [Constraint] -> Solver m Subst
solve [] = Solver m Subst
forall (f :: * -> *) a. (Applicative f, Monoid a) => f a
stub
solve [Constraint]
cs = (Constraint, [Constraint]) -> Solver m Subst
forall (m :: * -> *).
MonadState InferState m =>
(Constraint, [Constraint]) -> Solver m Subst
solve' ((Constraint, [Constraint]) -> Solver m Subst)
-> (Constraint, [Constraint]) -> Solver m Subst
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) =
    [Constraint] -> Solver m Subst
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) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
cs)
  solve' (ExpInstConst Type
t Scheme
s, [Constraint]
cs) =
    do
      Type
s' <- m Type -> Solver m Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Type -> Solver m Type) -> m Type -> Solver m Type
forall a b. (a -> b) -> a -> b
$ Scheme -> m Type
forall (m :: * -> *). MonadState InferState m => Scheme -> m Type
instantiate Scheme
s
      [Constraint] -> Solver m Subst
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve (Type -> Type -> Constraint
EqConst Type
t Type
s' Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
cs)
  solve' (EqConst Type
t1 Type
t2, [Constraint]
cs) =
    (\ Subst
su1 ->
      (Subst -> Solver m Subst
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> Solver m Subst)
-> (Subst -> Subst) -> Subst -> Solver m Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Subst -> Subst
compose Subst
su1) (Subst -> Solver m Subst) -> Solver m Subst -> Solver m Subst
forall (m :: * -> *) a b.
Monad m =>
(a -> Solver m b) -> Solver m a -> Solver m b
-<< [Constraint] -> Solver m Subst
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve ((Subst -> [Constraint] -> [Constraint]
forall a. Substitutable a => Subst -> a -> a
`apply` [Constraint]
cs) Subst
su1)
    ) (Subst -> Solver m Subst) -> Solver m Subst -> Solver m Subst
forall (m :: * -> *) a b.
Monad m =>
(a -> Solver m b) -> Solver m a -> Solver m b
-<<
    Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2

infixr 1 -<<
-- | @LogicT@ fair conjunction, since library has only @>>-@
(-<<) :: Monad m => (a -> Solver m b) -> Solver m a -> Solver m b
-<< :: (a -> Solver m b) -> Solver m a -> Solver m b
(-<<) = (Solver m a -> (a -> Solver m b) -> Solver m b)
-> (a -> Solver m b) -> Solver m a -> Solver m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip Solver m a -> (a -> Solver m b) -> Solver m b
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
(>>-)