{-# LANGUAGE CPP #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

module Nix.Type.Infer
  ( Constraint(..)
  , TypeError(..)
  , InferError(..)
  , Subst(..)
  , inferTop
  )
where

import           Control.Applicative
import           Control.Arrow
import           Control.Monad.Catch
import           Control.Monad.Except
#if !MIN_VERSION_base(4,13,0)
import           Control.Monad.Fail
#endif
import           Control.Monad.Logic
import           Control.Monad.Reader
import           Control.Monad.Ref
import           Control.Monad.ST
import           Control.Monad.State.Strict
import           Data.Fix                       ( foldFix )
import           Data.Foldable
import qualified Data.HashMap.Lazy             as M
import           Data.List                      ( delete
                                                , nub
                                                , intersect
                                                , (\\)
                                                )
import           Data.Map                       ( Map )
import qualified Data.Map                      as Map
import           Data.Maybe                     ( fromJust )
import qualified Data.Set                      as Set
import           Data.Text                      ( Text )
import           Nix.Atoms
import           Nix.Convert
import           Nix.Eval                       ( MonadEval(..) )
import qualified Nix.Eval                      as Eval
import           Nix.Expr.Types
import           Nix.Expr.Types.Annotated
import           Nix.Fresh
import           Nix.String
import           Nix.Scope
import qualified Nix.Type.Assumption           as As
import           Nix.Type.Env
import qualified Nix.Type.Env                  as Env
import           Nix.Type.Type
import           Nix.Utils
import           Nix.Value.Monad
import           Nix.Var

---------------------------------------------------------------------------------
-- * Classes
---------------------------------------------------------------------------------

-- | Inference monad
newtype InferT s m a = InferT
    { InferT s m a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
getInfer ::
        ReaderT (Set.Set TVar, Scopes (InferT s m) (Judgment s))
            (StateT InferState (ExceptT InferError 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
        )

instance MonadTrans (InferT s) where
  lift :: m a -> InferT s m a
lift = ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
forall s (m :: * -> *) a.
ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
InferT (ReaderT
   (Set TVar, Scopes (InferT s m) (Judgment s))
   (StateT InferState (ExceptT InferError m))
   a
 -> InferT s m a)
-> (m a
    -> ReaderT
         (Set TVar, Scopes (InferT s m) (Judgment s))
         (StateT InferState (ExceptT InferError m))
         a)
-> m a
-> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT InferState (ExceptT InferError m) a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT InferState (ExceptT InferError m) a
 -> ReaderT
      (Set TVar, Scopes (InferT s m) (Judgment s))
      (StateT InferState (ExceptT InferError m))
      a)
-> (m a -> StateT InferState (ExceptT InferError m) a)
-> m a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError 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 MonadThunkId m => MonadThunkId (InferT s m) where
--   type ThunkId (InferT s m) = ThunkId m

-- | Inference state
newtype InferState = InferState { InferState -> Int
count :: Int }

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

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)

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)

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

instance Substitutable TVar where
  apply :: Subst -> TVar -> TVar
apply (Subst Map TVar Type
s) TVar
a = TVar
tv
   where
    t :: Type
t         = TVar -> Type
TVar TVar
a
    (TVar TVar
tv) = 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

instance Substitutable Type where
  apply :: Subst -> Type -> Type
apply Subst
_         (  TCon String
a   ) = String -> Type
TCon String
a
  apply Subst
s         (  TSet Bool
b AttrSet Type
a ) = Bool -> AttrSet Type -> Type
TSet Bool
b ((Type -> Type) -> AttrSet Type -> AttrSet Type
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s) AttrSet Type
a)
  apply Subst
s         (  TList [Type]
a  ) = [Type] -> Type
TList ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s) [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) = Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t1 Type -> Type -> Type
:~> Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t2
  apply Subst
s         (  TMany [Type]
ts ) = [Type] -> Type
TMany ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s) [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
EqConst (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t1) (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s 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 a b. (a -> b) -> [a] -> [b]
map ((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


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

instance FreeTypeVars Type where
  ftv :: Type -> Set TVar
ftv TCon{}      = Set TVar
forall a. Set a
Set.empty
  ftv (TVar TVar
a   ) = TVar -> Set TVar
forall a. a -> Set a
Set.singleton TVar
a
  ftv (TSet Bool
_ AttrSet Type
a ) = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Type -> Set TVar) -> [Type] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv (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 ((Type -> Set TVar) -> [Type] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv [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. Ord a => Set a -> Set a -> Set a
`Set.union` 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 ((Type -> Set TVar) -> [Type] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set TVar
forall a. FreeTypeVars a => a -> Set TVar
ftv [Type]
ts)

instance FreeTypeVars TVar where
  ftv :: TVar -> Set TVar
ftv = TVar -> Set TVar
forall a. a -> Set a
Set.singleton

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. Ord a => Set a -> Set a -> Set a
Set.union (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. Set a
Set.empty

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. Ord a => Set a -> Set a -> Set a
Set.union (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. Set a
Set.empty


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

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. Ord a => Set a -> Set a -> Set a
`Set.union` 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. Ord a => Set a -> Set a -> Set a
`Set.union` (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. Ord a => Set a -> Set a -> Set a
`Set.union` 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. Ord a => Set a -> Set a -> Set a
Set.union (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. Set a
Set.empty

data TypeError
  = UnificationFail Type Type
  | InfiniteType TVar Type
  | UnboundVariables [Text]
  | 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)

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
err]

deriving instance Show InferError
instance Exception InferError

instance Semigroup InferError where
  InferError
x <> :: InferError -> InferError -> InferError
<> InferError
_ = InferError
x

instance Monoid InferError where
  mempty :: InferError
mempty  = InferError
TypeInferenceAborted
  mappend :: InferError -> InferError -> InferError
mappend = InferError -> InferError -> InferError
forall a. Semigroup a => a -> a -> a
(<>)

---------------------------------------------------------------------------------
-- * Inference
---------------------------------------------------------------------------------

-- | 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
forall a. Set a
Set.empty, Scopes (InferT s m) (Judgment s)
forall (m :: * -> *) a. Scopes m a
emptyScopes))
    (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
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError 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
$ do
  STRef s Int
i <- Int -> ST s (Ref (ST s) Int)
forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newVar (Int
1 :: Int)
  Ref (ST s) Int
-> FreshIdT Int (ST s) (Either InferError a)
-> ST s (Either InferError a)
forall (m :: * -> *) i a.
Functor m =>
Var m i -> FreshIdT i m a -> m a
runFreshIdT STRef s Int
Ref (ST s) Int
i (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)

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 Name
unbounds =
        [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList (Assumption -> [Name]
As.keys Assumption
as) Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList (Env -> [Name]
Env.keys Env
env)
  Bool -> InferT s m () -> InferT s m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
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
$ [Name] -> TypeError
UnboundVariables
    ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
unbounds))
  let cs' :: [Constraint]
cs' =
        [ Type -> Scheme -> Constraint
ExpInstConst Type
t Scheme
s
        | (Name
x, [Scheme]
ss) <- Env -> [(Name, [Scheme])]
Env.toList Env
env
        , Scheme
s       <- [Scheme]
ss
        , Type
t       <- Name -> Assumption -> [Type]
As.lookup Name
x Assumption
as
        ]
  InferState
inferState <- InferT s m InferState
forall s (m :: * -> *). MonadState s m => m s
get
  let eres :: Either [TypeError] [(Subst, Type)]
eres = (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)])
-> State InferState (Either [TypeError] [(Subst, Type)])
-> Either [TypeError] [(Subst, Type)]
forall a b. (a -> b) -> a -> b
$ 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)
 -> State InferState (Either [TypeError] [(Subst, Type)]))
-> Solver (StateT InferState Identity) (Subst, Type)
-> State InferState (Either [TypeError] [(Subst, Type)])
forall a b. (a -> b) -> a -> b
$ do
        Subst
subst <- [Constraint] -> Solver (StateT InferState Identity) Subst
forall (m :: * -> *).
MonadState InferState m =>
[Constraint] -> Solver m Subst
solve ([Constraint]
cs [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs')
        (Subst, Type) -> Solver (StateT InferState Identity) (Subst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, Subst
subst Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
`apply` Type
t)
  case Either [TypeError] [(Subst, Type)]
eres of
    Left  [TypeError]
errs -> InferError -> InferT s m [(Subst, Type)]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InferError -> InferT s m [(Subst, Type)])
-> InferError -> InferT s m [(Subst, Type)]
forall a b. (a -> b) -> a -> b
$ [TypeError] -> InferError
TypeInferenceErrors [TypeError]
errs
    Right [(Subst, Type)]
xs   -> [(Subst, Type)] -> InferT s m [(Subst, Type)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Subst, Type)]
xs

-- | 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 = case (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) of
  Left  InferError
err -> InferError -> Either InferError [Scheme]
forall a b. a -> Either a b
Left InferError
err
  Right [(Subst, Type)]
xs  -> [Scheme] -> Either InferError [Scheme]
forall a b. b -> Either a b
Right ([Scheme] -> Either InferError [Scheme])
-> [Scheme] -> Either InferError [Scheme]
forall a b. (a -> b) -> a -> b
$ ((Subst, Type) -> Scheme) -> [(Subst, Type)] -> [Scheme]
forall a b. (a -> b) -> [a] -> [b]
map (\(Subst
subst, Type
ty) -> Type -> Scheme
closeOver (Subst
subst Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
`apply` Type
ty)) [(Subst, Type)]
xs

-- | 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. Set a
Set.empty

extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
extendMSet :: TVar -> InferT s m a -> InferT s m a
extendMSet TVar
x = ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
forall s (m :: * -> *) a.
ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
InferT (ReaderT
   (Set TVar, Scopes (InferT s m) (Judgment s))
   (StateT InferState (ExceptT InferError m))
   a
 -> InferT s 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
-> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Set TVar, Scopes (InferT s m) (Judgment s))
 -> (Set TVar, Scopes (InferT s m) (Judgment s)))
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError 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 (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TVar -> Set TVar -> Set TVar
forall a. Ord a => a -> Set a -> Set a
Set.insert TVar
x)) (ReaderT
   (Set TVar, Scopes (InferT s m) (Judgment s))
   (StateT InferState (ExceptT InferError m))
   a
 -> ReaderT
      (Set TVar, Scopes (InferT s m) (Judgment s))
      (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
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (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
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
getInfer

letters :: [String]
letters :: [String]
letters = [Int
1 ..] [Int] -> (Int -> [String]) -> [String]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Int -> String -> [String]) -> String -> Int -> [String]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> String -> [String]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM [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
s { count :: Int
count = InferState -> Int
count InferState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
  TVar -> m TVar
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar -> m TVar) -> TVar -> m TVar
forall a b. (a -> b) -> a -> b
$ String -> TVar
TV ([String]
letters [String] -> Int -> String
forall a. [a] -> Int -> a
!! InferState -> Int
count 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

instantiate :: MonadState InferState m => Scheme -> m Type
instantiate :: Scheme -> m Type
instantiate (Forall [TVar]
as Type
t) = do
  [Type]
as' <- (TVar -> m Type) -> [TVar] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m Type -> TVar -> m Type
forall a b. a -> b -> a
const m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh) [TVar]
as
  let s :: Subst
s = Map TVar Type -> Subst
Subst (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ [(TVar, Type)] -> Map TVar Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, Type)] -> Map TVar Type)
-> [(TVar, Type)] -> Map TVar Type
forall a b. (a -> b) -> a -> b
$ [TVar] -> [Type] -> [(TVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as [Type]
as'
  Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply Subst
s Type
t

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
$ 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` Set TVar
free

unops :: Type -> NUnaryOp -> [Constraint]
unops :: Type -> NUnaryOp -> [Constraint]
unops Type
u1 = \case
  NUnaryOp
NNot -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeBool, Type
typeBool])]
  NUnaryOp
NNeg ->
    [ Type -> Type -> Constraint
EqConst
        Type
u1
        ([Type] -> Type
TMany [[Type] -> Type
typeFun [Type
typeInt, Type
typeInt], [Type] -> Type
typeFun [Type
typeFloat, Type
typeFloat]])
    ]

binops :: Type -> NBinaryOp -> [Constraint]
binops :: Type -> NBinaryOp -> [Constraint]
binops Type
u1 = \case
  NBinaryOp
NApp  -> []                -- this is handled separately

  -- Equality tells you nothing about the types, because any two types are
  -- allowed.
  NBinaryOp
NEq   -> []
  NBinaryOp
NNEq  -> []

  NBinaryOp
NGt   -> [Constraint]
inequality
  NBinaryOp
NGte  -> [Constraint]
inequality
  NBinaryOp
NLt   -> [Constraint]
inequality
  NBinaryOp
NLte  -> [Constraint]
inequality

  NBinaryOp
NAnd  -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeBool, Type
typeBool, Type
typeBool])]
  NBinaryOp
NOr   -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeBool, Type
typeBool, Type
typeBool])]
  NBinaryOp
NImpl -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeBool, Type
typeBool, Type
typeBool])]

  NBinaryOp
NConcat -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeList, Type
typeList, Type
typeList])]

  NBinaryOp
NUpdate ->
    [ Type -> Type -> Constraint
EqConst
        Type
u1
        ([Type] -> Type
TMany
          [ [Type] -> Type
typeFun [Type
typeSet, Type
typeSet, Type
typeSet]
          , [Type] -> Type
typeFun [Type
typeSet, Type
typeNull, Type
typeSet]
          , [Type] -> Type
typeFun [Type
typeNull, Type
typeSet, Type
typeSet]
          ]
        )
    ]

  NBinaryOp
NPlus ->
    [ Type -> Type -> Constraint
EqConst
        Type
u1
        ([Type] -> Type
TMany
          [ [Type] -> Type
typeFun [Type
typeInt, Type
typeInt, Type
typeInt]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeFloat, Type
typeFloat]
          , [Type] -> Type
typeFun [Type
typeInt, Type
typeFloat, Type
typeFloat]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeInt, Type
typeFloat]
          , [Type] -> Type
typeFun [Type
typeString, Type
typeString, Type
typeString]
          , [Type] -> Type
typeFun [Type
typePath, Type
typePath, Type
typePath]
          , [Type] -> Type
typeFun [Type
typeString, Type
typeString, Type
typePath]
          ]
        )
    ]
  NBinaryOp
NMinus -> [Constraint]
arithmetic
  NBinaryOp
NMult  -> [Constraint]
arithmetic
  NBinaryOp
NDiv   -> [Constraint]
arithmetic
 where
  inequality :: [Constraint]
inequality =
    [ Type -> Type -> Constraint
EqConst
        Type
u1
        ([Type] -> Type
TMany
          [ [Type] -> Type
typeFun [Type
typeInt, Type
typeInt, Type
typeBool]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeFloat, Type
typeBool]
          , [Type] -> Type
typeFun [Type
typeInt, Type
typeFloat, Type
typeBool]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeInt, Type
typeBool]
          ]
        )
    ]

  arithmetic :: [Constraint]
arithmetic =
    [ Type -> Type -> Constraint
EqConst
        Type
u1
        ([Type] -> Type
TMany
          [ [Type] -> Type
typeFun [Type
typeInt, Type
typeInt, Type
typeInt]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeFloat, Type
typeFloat]
          , [Type] -> Type
typeFun [Type
typeInt, Type
typeFloat, Type
typeFloat]
          , [Type] -> Type
typeFun [Type
typeFloat, Type
typeInt, Type
typeFloat]
          ]
        )
    ]

liftInfer :: Monad m => m a -> InferT s m a
liftInfer :: m a -> InferT s m a
liftInfer = ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
forall s (m :: * -> *) a.
ReaderT
  (Set TVar, Scopes (InferT s m) (Judgment s))
  (StateT InferState (ExceptT InferError m))
  a
-> InferT s m a
InferT (ReaderT
   (Set TVar, Scopes (InferT s m) (Judgment s))
   (StateT InferState (ExceptT InferError m))
   a
 -> InferT s m a)
-> (m a
    -> ReaderT
         (Set TVar, Scopes (InferT s m) (Judgment s))
         (StateT InferState (ExceptT InferError m))
         a)
-> m a
-> InferT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT InferState (ExceptT InferError m) a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError m))
     a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT InferState (ExceptT InferError m) a
 -> ReaderT
      (Set TVar, Scopes (InferT s m) (Judgment s))
      (StateT InferState (ExceptT InferError m))
      a)
-> (m a -> StateT InferState (ExceptT InferError m) a)
-> m a
-> ReaderT
     (Set TVar, Scopes (InferT s m) (Judgment s))
     (StateT InferState (ExceptT InferError 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, 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)
    b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res

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

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
      (String -> InferT s m a
forall a. HasCallStack => String -> a
error (String -> InferT s m a) -> String -> InferT s m a
forall a b. (a -> b) -> a -> b
$ String
"Exception was not an exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ s -> String
forall a. Show a => a -> String
show s
e)
      e -> InferT s m a
h
      (SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
fromException (s -> SomeException
forall e. Exception e => e -> SomeException
toException s
e))
    InferError
err -> String -> InferT s m a
forall a. HasCallStack => String -> a
error (String -> InferT s m a) -> String -> InferT s m a
forall a b. (a -> b) -> a -> b
$ String
"Unexpected error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InferError -> String
forall a. Show a => a -> String
show InferError
err

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

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)
forall a. a -> a
id
  demand :: Judgment s -> (Judgment s -> InferT s m r) -> InferT s m r
demand = ((Judgment s -> InferT s m r) -> Judgment s -> InferT s m r)
-> Judgment s -> (Judgment s -> InferT s m r) -> InferT s m r
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Judgment s -> InferT s m r) -> Judgment s -> InferT s m r
forall a b. (a -> b) -> a -> b
($)
  inform :: Judgment s
-> (InferT s m (Judgment s) -> InferT s m (Judgment s))
-> InferT s m (Judgment s)
inform Judgment s
j InferT s m (Judgment s) -> InferT s m (Judgment s)
f = InferT s m (Judgment s) -> InferT s m (Judgment s)
f (Judgment s -> InferT s m (Judgment s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Judgment s
j)

{-
instance MonadInfer m
  => MonadThunk (JThunkT s m) (InferT s m) (Judgment s) where
  thunk = fmap JThunk . thunk
  thunkId (JThunk x) = thunkId x

  queryM (JThunk x) b f = queryM x b f

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

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

instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
  freeVariable :: Name -> InferT s m (Judgment s)
freeVariable Name
var = do
    Type
tv <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 (Name -> Type -> Assumption
As.singleton Name
var Type
tv) [] Type
tv

  synHole :: Name -> InferT s m (Judgment s)
synHole Name
var = do
    Type
tv <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 (Name -> Type -> Assumption
As.singleton Name
var Type
tv) [] Type
tv

-- If we fail to look up an attribute, we just don't know the type.
  attrMissing :: NonEmpty Name -> Maybe (Judgment s) -> InferT s m (Judgment s)
attrMissing NonEmpty Name
_ Maybe (Judgment s)
_ = Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
As.empty [] (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 :: Name -> Judgment s -> InferT s m (Judgment s)
evaledSym Name
_ = 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 (m :: * -> *) a. Monad m => a -> m a
return (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.empty [] (Type -> Judgment s) -> Type -> Judgment s
forall a b. (a -> b) -> a -> b
$ Bool -> AttrSet Type -> Type
TSet Bool
False (AttrSet Type -> Type) -> AttrSet Type -> Type
forall a b. (a -> b) -> a -> b
$ [(Name, Type)] -> AttrSet Type
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
    [(Name
"file", Type
typePath), (Name
"line", Type
typeInt), (Name
"col", Type
typeInt)]

  evalConstant :: NAtom -> InferT s m (Judgment s)
evalConstant NAtom
c = Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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.empty [] (NAtom -> Type
go NAtom
c)
   where
    go :: NAtom -> Type
go = \case
      NURI   Name
_ -> 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      = InferT s m (Judgment s)
-> NString (InferT s m (Judgment s)) -> InferT s m (Judgment s)
forall a b. a -> b -> a
const (InferT s m (Judgment s)
 -> NString (InferT s m (Judgment s)) -> InferT s m (Judgment s))
-> InferT s m (Judgment s)
-> NString (InferT s m (Judgment s))
-> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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.empty [] Type
typeString
  evalLiteralPath :: String -> InferT s m (Judgment s)
evalLiteralPath = InferT s m (Judgment s) -> String -> InferT s m (Judgment s)
forall a b. a -> b -> a
const (InferT s m (Judgment s) -> String -> InferT s m (Judgment s))
-> InferT s m (Judgment s) -> String -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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.empty [] Type
typePath
  evalEnvPath :: String -> InferT s m (Judgment s)
evalEnvPath     = InferT s m (Judgment s) -> String -> InferT s m (Judgment s)
forall a b. a -> b -> a
const (InferT s m (Judgment s) -> String -> InferT s m (Judgment s))
-> InferT s m (Judgment s) -> String -> InferT s m (Judgment s)
forall a b. (a -> b) -> a -> b
$ Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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.empty [] Type
typePath

  evalUnary :: NUnaryOp -> Judgment s -> InferT s m (Judgment s)
evalUnary NUnaryOp
op (Judgment Assumption
as1 [Constraint]
cs1 Type
t1) = do
    Type
tv <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ Type -> NUnaryOp -> [Constraint]
unops (Type
t1 Type -> Type -> Type
:~> Type
tv) NUnaryOp
op) Type
tv

  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
    Type
tv                  <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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
`As.merge` Assumption
as2)
                      ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ Type -> NBinaryOp -> [Constraint]
binops (Type
t1 Type -> Type -> Type
:~> Type
t2 Type -> Type -> Type
:~> Type
tv) NBinaryOp
op)
                      Type
tv

  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 (m :: * -> *) a. Monad m => a -> m a
return (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
`As.merge` Assumption
as2 Assumption -> Assumption -> Assumption
`As.merge` Assumption
as3)
      ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs3 [Constraint] -> [Constraint] -> [Constraint]
forall 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 (m :: * -> *) a. Monad m => a -> m a
return
      (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
`As.merge` Assumption
as2) ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [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
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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
`As.merge` Assumption
as2)
                      ([Constraint]
cs1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
cs2 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [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 Name
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 (m :: * -> *) s a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet
      TVar
a
      (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 (Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment (Name -> Type -> Assumption
As.singleton Name
x Type
tv) [] Type
tv)) (\AttrSet (InferT s m (Judgment s))
_ InferT s m (Judgment s)
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
<$> InferT s m (Judgment s)
b))
    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> Name -> Assumption
`As.remove` Name
x)
                      ([Constraint]
cs [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [ Type -> Type -> Constraint
EqConst Type
t' Type
tv | Type
t' <- Name -> Assumption -> [Type]
As.lookup Name
x Assumption
as ])
                      (Type
tv Type -> Type -> Type
:~> Type
t)

  evalAbs (ParamSet ParamSet (InferT s m (Judgment s))
ps Bool
variadic Maybe Name
_mname) 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
    [(Name, Type)]
js <- ([[(Name, Type)]] -> [(Name, Type)])
-> InferT s m [[(Name, Type)]] -> InferT s m [(Name, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(Name, Type)]] -> [(Name, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (InferT s m [[(Name, Type)]] -> InferT s m [(Name, Type)])
-> InferT s m [[(Name, Type)]] -> InferT s m [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ ParamSet (InferT s m (Judgment s))
-> ((Name, Maybe (InferT s m (Judgment s)))
    -> InferT s m [(Name, Type)])
-> InferT s m [[(Name, Type)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ParamSet (InferT s m (Judgment s))
ps (((Name, Maybe (InferT s m (Judgment s)))
  -> InferT s m [(Name, Type)])
 -> InferT s m [[(Name, Type)]])
-> ((Name, Maybe (InferT s m (Judgment s)))
    -> InferT s m [(Name, Type)])
-> InferT s m [[(Name, Type)]]
forall a b. (a -> b) -> a -> b
$ \(Name
name, Maybe (InferT s m (Judgment s))
_) -> do
      Type
tv <- InferT s m Type
forall (m :: * -> *). MonadState InferState m => m Type
fresh
      [(Name, Type)] -> InferT s m [(Name, Type)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Name
name, Type
tv)]

    let (Assumption
env, AttrSet Type
tys) =
          (\(Assumption, AttrSet Type)
-> (Name, Type) -> (Assumption, AttrSet Type)
f -> ((Assumption, AttrSet Type)
 -> (Name, Type) -> (Assumption, AttrSet Type))
-> (Assumption, AttrSet Type)
-> [(Name, Type)]
-> (Assumption, AttrSet Type)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Assumption, AttrSet Type)
-> (Name, Type) -> (Assumption, AttrSet Type)
f (Assumption
As.empty, AttrSet Type
forall k v. HashMap k v
M.empty) [(Name, Type)]
js) (((Assumption, AttrSet Type)
  -> (Name, Type) -> (Assumption, AttrSet Type))
 -> (Assumption, AttrSet Type))
-> ((Assumption, AttrSet Type)
    -> (Name, Type) -> (Assumption, AttrSet Type))
-> (Assumption, AttrSet Type)
forall a b. (a -> b) -> a -> b
$ \(Assumption
as1, AttrSet Type
t1) (Name
k, Type
t) ->
            (Assumption
as1 Assumption -> Assumption -> Assumption
`As.merge` Name -> Type -> Assumption
As.singleton Name
k Type
t, Name -> Type -> AttrSet Type -> AttrSet Type
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Name
k Type
t AttrSet Type
t1)
        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 [] (Bool -> AttrSet Type -> Type
TSet Bool
True 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 :: [Name]
names = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
js

    (AttrSet (InferT s m (Judgment s))
args, Judgment Assumption
as [Constraint]
cs Type
t) <- ((Name, 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)
-> [(Name, 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 (\(Name
_, TVar TVar
a) -> TVar
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
-> InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
forall (m :: * -> *) s a.
Monad m =>
TVar -> InferT s m a -> InferT s m a
extendMSet TVar
a) InferT s m (AttrSet (InferT s m (Judgment s)), Judgment s)
call [(Name, Type)]
js

    Type
ty <- Bool -> AttrSet Type -> Type
TSet Bool
variadic (AttrSet Type -> Type)
-> InferT s m (AttrSet Type) -> InferT s m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (InferT s m (Judgment s) -> InferT s m Type)
-> AttrSet (InferT s m (Judgment s)) -> InferT s m (AttrSet Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Judgment s -> Type
forall s. Judgment s -> Type
inferredType (Judgment s -> Type) -> InferT s m (Judgment s) -> InferT s m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) AttrSet (InferT s m (Judgment s))
args

    Judgment s -> InferT s m (Judgment s)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> Name -> Assumption)
-> Assumption -> [Name] -> Assumption
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Assumption -> Name -> Assumption
As.remove Assumption
as [Name]
names)
      ([Constraint]
cs [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [ Type -> Type -> Constraint
EqConst Type
t' (AttrSet Type
tys AttrSet Type -> Name -> Type
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Name
x) | Name
x <- [Name]
names, Type
t' <- Name -> Assumption -> [Type]
As.lookup Name
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

data Judgment s = Judgment
    { Judgment s -> Assumption
assumptions     :: As.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

instance Monad m => FromValue NixString (InferT s m) (Judgment s) where
  fromValueMay :: Judgment s -> InferT s m (Maybe NixString)
fromValueMay Judgment s
_ = Maybe NixString -> InferT s m (Maybe NixString)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe NixString
forall a. Maybe a
Nothing
  fromValue :: Judgment s -> InferT s m NixString
fromValue Judgment s
_ = String -> InferT s m NixString
forall a. HasCallStack => String -> a
error String
"Unused"

instance MonadInfer m
  => FromValue (AttrSet (Judgment s), AttrSet SourcePos)
              (InferT s m) (Judgment s) where
  fromValueMay :: Judgment s
-> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos))
fromValueMay (Judgment Assumption
_ [Constraint]
_ (TSet Bool
_ AttrSet Type
xs)) = do
    let sing :: p -> Type -> Judgment s
sing p
_ = Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
As.empty []
    Maybe (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (AttrSet (Judgment s), AttrSet SourcePos)
 -> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos)))
-> Maybe (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos))
forall a b. (a -> b) -> a -> b
$ (AttrSet (Judgment s), AttrSet SourcePos)
-> Maybe (AttrSet (Judgment s), AttrSet SourcePos)
forall a. a -> Maybe a
Just ((Name -> Type -> Judgment s)
-> AttrSet Type -> AttrSet (Judgment s)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey Name -> Type -> Judgment s
forall p s. p -> Type -> Judgment s
sing AttrSet Type
xs, AttrSet SourcePos
forall k v. HashMap k v
M.empty)
  fromValueMay Judgment s
_ = Maybe (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (AttrSet (Judgment s), AttrSet SourcePos)
forall a. Maybe a
Nothing
  fromValue :: Judgment s -> InferT s m (AttrSet (Judgment s), AttrSet SourcePos)
fromValue = Judgment s
-> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos))
forall a (m :: * -> *) v. FromValue a m v => v -> m (Maybe a)
fromValueMay (Judgment s
 -> InferT s m (Maybe (AttrSet (Judgment s), AttrSet SourcePos)))
-> (Maybe (AttrSet (Judgment s), AttrSet SourcePos)
    -> InferT s m (AttrSet (Judgment s), AttrSet SourcePos))
-> Judgment s
-> InferT s m (AttrSet (Judgment s), AttrSet SourcePos)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    Just (AttrSet (Judgment s), AttrSet SourcePos)
v  -> (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (AttrSet (Judgment s), AttrSet SourcePos)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttrSet (Judgment s), AttrSet SourcePos)
v
    Maybe (AttrSet (Judgment s), AttrSet SourcePos)
Nothing -> (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (AttrSet (Judgment s), AttrSet SourcePos)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttrSet (Judgment s)
forall k v. HashMap k v
M.empty, AttrSet SourcePos
forall k v. HashMap k v
M.empty)

instance MonadInfer m
  => ToValue (AttrSet (Judgment s), AttrSet SourcePos)
            (InferT s m) (Judgment s) where
  toValue :: (AttrSet (Judgment s), AttrSet SourcePos)
-> InferT s m (Judgment s)
toValue (AttrSet (Judgment s)
xs, AttrSet SourcePos
_) =
    Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
      (Assumption -> [Constraint] -> Type -> Judgment s)
-> InferT s m Assumption
-> InferT s m ([Constraint] -> Type -> Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> Assumption -> InferT s m Assumption)
-> Assumption -> AttrSet (Judgment s) -> InferT s m Assumption
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Judgment s -> Assumption -> InferT s m Assumption
forall s (m :: * -> *).
(MonadValue (Judgment s) m, Applicative m) =>
Judgment s -> Assumption -> m Assumption
go Assumption
As.empty AttrSet (Judgment s)
xs
      InferT s m ([Constraint] -> Type -> Judgment s)
-> InferT s m [Constraint] -> InferT s m (Type -> Judgment s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (HashMap Name [Constraint] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (HashMap Name [Constraint] -> [Constraint])
-> InferT s m (HashMap Name [Constraint])
-> InferT s m [Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> InferT s m [Constraint])
-> AttrSet (Judgment s) -> InferT s m (HashMap Name [Constraint])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Judgment s
-> (Judgment s -> InferT s m [Constraint])
-> InferT s m [Constraint]
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
`demand` ([Constraint] -> InferT s m [Constraint]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Constraint] -> InferT s m [Constraint])
-> (Judgment s -> [Constraint])
-> Judgment s
-> InferT s m [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment s -> [Constraint]
forall s. Judgment s -> [Constraint]
typeConstraints)) AttrSet (Judgment s)
xs)
      InferT s m (Type -> Judgment s)
-> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Bool -> AttrSet Type -> Type
TSet Bool
True (AttrSet Type -> Type)
-> InferT s m (AttrSet Type) -> InferT s m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> InferT s m Type)
-> AttrSet (Judgment s) -> InferT s m (AttrSet Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Judgment s -> (Judgment s -> InferT s m Type) -> InferT s m Type
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
`demand` (Type -> InferT s m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> InferT s m Type)
-> (Judgment s -> Type) -> Judgment s -> InferT s m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment s -> Type
forall s. Judgment s -> Type
inferredType)) AttrSet (Judgment s)
xs)
    where go :: Judgment s -> Assumption -> m Assumption
go Judgment s
x Assumption
rest = Judgment s -> (Judgment s -> m Assumption) -> m Assumption
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Judgment s
x ((Judgment s -> m Assumption) -> m Assumption)
-> (Judgment s -> m Assumption) -> m Assumption
forall a b. (a -> b) -> a -> b
$ \Judgment s
x' -> Assumption -> m Assumption
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Assumption -> m Assumption) -> Assumption -> m Assumption
forall a b. (a -> b) -> a -> b
$ Assumption -> Assumption -> Assumption
As.merge (Judgment s -> Assumption
forall s. Judgment s -> Assumption
assumptions Judgment s
x') Assumption
rest

instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
  toValue :: [Judgment s] -> InferT s m (Judgment s)
toValue [Judgment s]
xs =
    Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment
      (Assumption -> [Constraint] -> Type -> Judgment s)
-> InferT s m Assumption
-> InferT s m ([Constraint] -> Type -> Judgment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> Assumption -> InferT s m Assumption)
-> Assumption -> [Judgment s] -> InferT s m Assumption
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Judgment s -> Assumption -> InferT s m Assumption
forall s (m :: * -> *).
(MonadValue (Judgment s) m, Applicative m) =>
Judgment s -> Assumption -> m Assumption
go Assumption
As.empty [Judgment s]
xs
      InferT s m ([Constraint] -> Type -> Judgment s)
-> InferT s m [Constraint] -> InferT s m (Type -> Judgment s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint]] -> [Constraint])
-> InferT s m [[Constraint]] -> InferT s m [Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> InferT s m [Constraint])
-> [Judgment s] -> InferT s m [[Constraint]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Judgment s
-> (Judgment s -> InferT s m [Constraint])
-> InferT s m [Constraint]
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
`demand` ([Constraint] -> InferT s m [Constraint]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Constraint] -> InferT s m [Constraint])
-> (Judgment s -> [Constraint])
-> Judgment s
-> InferT s m [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment s -> [Constraint]
forall s. Judgment s -> [Constraint]
typeConstraints)) [Judgment s]
xs)
      InferT s m (Type -> Judgment s)
-> InferT s m Type -> InferT s m (Judgment s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Type] -> Type
TList ([Type] -> Type) -> InferT s m [Type] -> InferT s m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Judgment s -> InferT s m Type)
-> [Judgment s] -> InferT s m [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Judgment s -> (Judgment s -> InferT s m Type) -> InferT s m Type
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
`demand` (Type -> InferT s m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> InferT s m Type)
-> (Judgment s -> Type) -> Judgment s -> InferT s m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment s -> Type
forall s. Judgment s -> Type
inferredType)) [Judgment s]
xs)
    where go :: Judgment s -> Assumption -> m Assumption
go Judgment s
x Assumption
rest = Judgment s -> (Judgment s -> m Assumption) -> m Assumption
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Judgment s
x ((Judgment s -> m Assumption) -> m Assumption)
-> (Judgment s -> m Assumption) -> m Assumption
forall a b. (a -> b) -> a -> b
$ \Judgment s
x' -> Assumption -> m Assumption
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Assumption -> m Assumption) -> Assumption -> m Assumption
forall a b. (a -> b) -> a -> b
$ Assumption -> Assumption -> Assumption
As.merge (Judgment s -> Assumption
forall s. Judgment s -> Assumption
assumptions Judgment s
x') Assumption
rest

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
$ Assumption -> [Constraint] -> Type -> Judgment s
forall s. Assumption -> [Constraint] -> Type -> Judgment s
Judgment Assumption
As.empty [] Type
typeBool

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 -> [(Text, NExpr)] -> Either InferError Env
inferTop :: Env -> [(Name, NExpr)] -> Either InferError Env
inferTop Env
env []                = Env -> Either InferError Env
forall a b. b -> Either a b
Right Env
env
inferTop Env
env ((Name
name, NExpr
ex) : [(Name, NExpr)]
xs) = case Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex of
  Left  InferError
err -> InferError -> Either InferError Env
forall a b. a -> Either a b
Left InferError
err
  Right [Scheme]
ty  -> Env -> [(Name, NExpr)] -> Either InferError Env
inferTop (Env -> (Name, [Scheme]) -> Env
extend Env
env (Name
name, [Scheme]
ty)) [(Name, NExpr)]
xs

normalizeScheme :: Scheme -> Scheme
normalizeScheme :: Scheme -> Scheme
normalizeScheme (Forall [TVar]
_ Type
body) = [TVar] -> Type -> Scheme
Forall (((TVar, TVar) -> TVar) -> [(TVar, TVar)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, TVar) -> TVar
forall a b. (a, b) -> b
snd [(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. Eq a => [a] -> [a]
nub ([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ Type -> [TVar]
fv Type
body) ((String -> TVar) -> [String] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map String -> TVar
TV [String]
letters)

  fv :: Type -> [TVar]
fv (TVar TVar
a  ) = [TVar
a]
  fv (Type
a :~> Type
b ) = Type -> [TVar]
fv Type
a [TVar] -> [TVar] -> [TVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TVar]
fv Type
b
  fv (TCon String
_  ) = []
  fv (TSet Bool
_ AttrSet Type
a) = (Type -> [TVar]) -> [Type] -> [TVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TVar]
fv (AttrSet Type -> [Type]
forall k v. HashMap k v -> [v]
M.elems AttrSet Type
a)
  fv (TList [Type]
a ) = (Type -> [TVar]) -> [Type] -> [TVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TVar]
fv [Type]
a
  fv (TMany [Type]
ts) = (Type -> [TVar]) -> [Type] -> [TVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TVar]
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 String
a  ) = String -> Type
TCon String
a
  normtype (TSet Bool
b AttrSet Type
a) = Bool -> AttrSet Type -> Type
TSet Bool
b ((Type -> Type) -> AttrSet Type -> AttrSet Type
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map Type -> Type
normtype AttrSet Type
a)
  normtype (TList [Type]
a ) = [Type] -> Type
TList ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
normtype [Type]
a)
  normtype (TMany [Type]
ts) = [Type] -> Type
TMany ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
normtype [Type]
ts)
  normtype (TVar  TVar
a ) = case TVar -> [(TVar, TVar)] -> Maybe TVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
Prelude.lookup TVar
a [(TVar, TVar)]
ord of
    Just TVar
x  -> TVar -> Type
TVar TVar
x
    Maybe TVar
Nothing -> String -> Type
forall a. HasCallStack => String -> a
error String
"type variable not in signature"

---------------------------------------------------------------------------------
-- * Constraint Solver
---------------------------------------------------------------------------------

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])

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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LogicT (StateT [TypeError] m) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  catchError :: Solver m a -> (TypeError -> Solver m a) -> Solver m a
catchError Solver m a
_ TypeError -> Solver m a
_ = String -> Solver m a
forall a. HasCallStack => String -> a
error String
"This is never used"

runSolver :: 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) = do
  ([a], [TypeError])
res <- 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) []
  Either [TypeError] [a] -> m (Either [TypeError] [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [TypeError] [a] -> m (Either [TypeError] [a]))
-> Either [TypeError] [a] -> m (Either [TypeError] [a])
forall a b. (a -> b) -> a -> b
$ case ([a], [TypeError])
res of
    (a
x : [a]
xs, [TypeError]
_ ) -> [a] -> Either [TypeError] [a]
forall a b. b -> Either a b
Right (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
    ([a]
_     , [TypeError]
es) -> [TypeError] -> Either [TypeError] [a]
forall a b. a -> Either a b
Left ([TypeError] -> [TypeError]
forall a. Eq a => [a] -> [a]
nub [TypeError]
es)

-- | The empty substitution
emptySubst :: Subst
emptySubst :: Subst
emptySubst = Subst
forall a. Monoid a => a
mempty

-- | Compose substitutions
compose :: Subst -> Subst -> Subst
Subst Map TVar Type
s1 compose :: Subst -> Subst -> Subst
`compose` Subst Map TVar Type
s2 =
  Map TVar Type -> Subst
Subst (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Map TVar Type -> Map TVar Type
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Subst -> Type -> Type
forall a. Substitutable a => Subst -> a -> a
apply (Map TVar Type -> Subst
Subst Map TVar Type
s1)) Map TVar Type
s2 Map TVar Type -> Map TVar Type -> Map TVar Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map TVar Type
s1

unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany :: [Type] -> [Type] -> Solver m Subst
unifyMany []         []         = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
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 (Subst -> [Type] -> [Type]
forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 [Type]
ts1) (Subst -> [Type] -> [Type]
forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 [Type]
ts2)
  Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
`compose` Subst
su1)
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

allSameType :: [Type] -> Bool
allSameType :: [Type] -> Bool
allSameType []           = Bool
True
allSameType [Type
_         ] = Bool
True
allSameType (Type
x : Type
y : [Type]
ys) = Type
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y Bool -> Bool -> Bool
&& [Type] -> Bool
allSameType (Type
y Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ys)

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  = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
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])
_              -> Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
  | [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
-- We assume that lists of different lengths containing various types cannot
-- 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 Bool
True AttrSet Type
_) (   TSet Bool
True AttrSet Type
_) = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifies (TSet Bool
False AttrSet Type
b) (TSet Bool
True AttrSet Type
s)
  | AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifies (TSet Bool
True AttrSet Type
s) (TSet Bool
False AttrSet Type
b)
  | AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifies (TSet Bool
False AttrSet Type
s) (TSet Bool
False AttrSet Type
b) | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
b [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ AttrSet Type -> [Name]
forall k v. HashMap k v -> [k]
M.keys AttrSet Type
s) =
  Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
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 -> Type -> Solver m Subst) -> Type -> Type -> Solver m Subst
forall (f :: * -> *) a b. Functor f => f (a -> b) -> a -> f b
?? 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

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     = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
         | 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 (m :: * -> *) a. Monad m => a -> m a
return (Map TVar Type -> Subst
Subst (Map TVar Type -> Subst) -> Map TVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> Map TVar Type
forall k a. k -> a -> Map k a
Map.singleton TVar
a Type
t)

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

nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable :: [Constraint] -> (Constraint, [Constraint])
nextSolvable [Constraint]
xs = Maybe (Constraint, [Constraint]) -> (Constraint, [Constraint])
forall a. HasCallStack => Maybe a -> a
fromJust (((Constraint, [Constraint]) -> Bool)
-> [(Constraint, [Constraint])] -> Maybe (Constraint, [Constraint])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Constraint, [Constraint]) -> Bool
forall a. ActiveTypeVars a => (Constraint, a) -> Bool
solvable ([Constraint] -> [(Constraint, [Constraint])]
forall a. Eq a => [a] -> [(a, [a])]
chooseOne [Constraint]
xs))
 where
  chooseOne :: [a] -> [(a, [a])]
chooseOne [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, a) -> Bool
solvable (EqConst{}     , a
_) = Bool
True
  solvable (ExpInstConst{}, a
_) = Bool
True
  solvable (ImpInstConst Type
_t1 Set TVar
ms Type
t2, a
cs) =
    Set TVar -> Bool
forall a. Set a -> Bool
Set.null ((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.difference` Set TVar
ms) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` a -> Set TVar
forall a. ActiveTypeVars a => a -> Set TVar
atv a
cs)

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

solve :: MonadState InferState m => [Constraint] -> Solver m Subst
solve :: [Constraint] -> Solver m Subst
solve [] = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
solve [Constraint]
cs = (Constraint, [Constraint]) -> Solver m Subst
forall (m :: * -> *).
MonadState InferState m =>
(Constraint, [Constraint]) -> Solver m Subst
solve' ([Constraint] -> (Constraint, [Constraint])
nextSolvable [Constraint]
cs)
 where
  solve' :: (Constraint, [Constraint]) -> Solver m Subst
solve' (EqConst Type
t1 Type
t2, [Constraint]
cs) = Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
t1 Type
t2
    Solver m Subst -> (Subst -> Solver m Subst) -> Solver m Subst
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- \Subst
su1 -> [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 Subst
su1 [Constraint]
cs) Solver m Subst -> (Subst -> Solver m Subst) -> Solver m Subst
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- \Subst
su2 -> Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
`compose` Subst
su1)

  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)

instance Monad m => Scoped (Judgment s) (InferT s m) where
  currentScopes :: InferT s m (Scopes (InferT s m) (Judgment s))
currentScopes = 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)
currentScopesReader
  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 :: Name -> InferT s m (Maybe (Judgment s))
lookupVar     = Name -> InferT s m (Maybe (Judgment s))
forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
Name -> m (Maybe a)
lookupVarReader