{-# 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 = 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 s :: Map TVar Type
s) a :: TVar
a = TVar
tv
   where
    t :: Type
t         = TVar -> Type
TVar TVar
a
    (TVar tv :: 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 _         (  TCon a :: String
a   ) = String -> Type
TCon String
a
  apply s :: Subst
s         (  TSet b :: Bool
b a :: 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 s :: Subst
s         (  TList a :: [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 s :: Map TVar Type
s) t :: Type
t@(TVar  a :: 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 s :: Subst
s         (  t1 :: Type
t1 :~> t2 :: 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 s :: Subst
s         (  TMany ts :: [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 s :: Map TVar Type
s) (Forall as :: [TVar]
as t :: 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 s :: Subst
s (EqConst      t1 :: Type
t1 t2 :: 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 s :: Subst
s (ExpInstConst t :: Type
t  sc :: 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 s :: Subst
s (ImpInstConst t1 :: Type
t1 ms :: Set TVar
ms t2 :: 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 a :: TVar
a   ) = TVar -> Set TVar
forall a. a -> Set a
Set.singleton TVar
a
  ftv (TSet _ a :: 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 a :: [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 (t1 :: Type
t1 :~> t2 :: 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 ts :: [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 as :: [TVar]
as t :: 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 t1 :: Type
t1 t2 :: 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 t1 :: Type
t1 ms :: Set TVar
ms t2 :: 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 t :: Type
t s :: 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 err :: 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
  x :: InferError
x <> :: 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 m :: 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 (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
env ex :: NExpr
ex = do
  Judgment as :: Assumption
as cs :: [Constraint]
cs t :: 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
        | (x :: Name
x, ss :: [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  errs :: [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 xs :: [(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
env ex :: 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  err :: InferError
err -> InferError -> Either InferError [Scheme]
forall a b. a -> Either a b
Left InferError
err
  Right xs :: [(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
subst, ty :: 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 x :: 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 = [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 ['a' .. '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
+ 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 as :: [TVar]
as t :: 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 free :: Set TVar
free t :: 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 u1 :: Type
u1 = \case
  NNot -> [Type -> Type -> Constraint
EqConst Type
u1 ([Type] -> Type
typeFun [Type
typeBool, Type
typeBool])]
  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 u1 :: Type
u1 = \case
  NApp  -> []                -- this is handled separately

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

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

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

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

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

  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]
          ]
        )
    ]
  NMinus -> [Constraint]
arithmetic
  NMult  -> [Constraint]
arithmetic
  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 x :: a
x = m (Ref m a) -> InferT s m (Ref (InferT s m) a)
forall (m :: * -> *) a s. Monad m => m a -> InferT s m a
liftInfer (m (Ref m a) -> InferT s m (Ref (InferT s m) a))
-> m (Ref m a) -> InferT s m (Ref (InferT s 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 x :: 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 x :: Ref (InferT s m) a
x y :: 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 x :: Ref (InferT s m) a
x f :: 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 m :: InferT s m a
m h :: 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 e :: 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
$ "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))
    err :: 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
$ "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 j :: Judgment s
j f :: 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 var :: 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 var :: 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 _ _ = 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 _ = 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
    [("file", Type
typePath), ("line", Type
typeInt), ("col", Type
typeInt)]

  evalConstant :: NAtom -> InferT s m (Judgment s)
evalConstant c :: 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   _ -> Type
typeString
      NInt   _ -> Type
typeInt
      NFloat _ -> Type
typeFloat
      NBool  _ -> Type
typeBool
      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 op :: NUnaryOp
op (Judgment as1 :: Assumption
as1 cs1 :: [Constraint]
cs1 t1 :: 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 op :: NBinaryOp
op (Judgment as1 :: Assumption
as1 cs1 :: [Constraint]
cs1 t1 :: Type
t1) e2 :: InferT s m (Judgment s)
e2 = do
    Judgment as2 :: Assumption
as2 cs2 :: [Constraint]
cs2 t2 :: 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 as1 :: Assumption
as1 cs1 :: [Constraint]
cs1 t1 :: Type
t1) t :: InferT s m (Judgment s)
t f :: InferT s m (Judgment s)
f = do
    Judgment as2 :: Assumption
as2 cs2 :: [Constraint]
cs2 t2 :: Type
t2 <- InferT s m (Judgment s)
t
    Judgment as3 :: Assumption
as3 cs3 :: [Constraint]
cs3 t3 :: 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 as1 :: Assumption
as1 cs1 :: [Constraint]
cs1 t1 :: Type
t1) body :: InferT s m (Judgment s)
body = do
    Judgment as2 :: Assumption
as2 cs2 :: [Constraint]
cs2 t2 :: 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 as1 :: Assumption
as1 cs1 :: [Constraint]
cs1 t1 :: Type
t1) e2 :: InferT s m (Judgment s)
e2 = do
    Judgment as2 :: Assumption
as2 cs2 :: [Constraint]
cs2 t2 :: 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 x :: Name
x) k :: 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 as :: Assumption
as cs :: [Constraint]
cs t :: 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)) (\_ b :: 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 ps :: ParamSet (InferT s m (Judgment s))
ps variadic :: Bool
variadic _mname :: Maybe Name
_mname) k :: 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
name, _) -> 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 (env :: Assumption
env, tys :: AttrSet Type
tys) =
          (\f :: (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
$ \(as1 :: Assumption
as1, t1 :: AttrSet Type
t1) (k :: Name
k, t :: 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
$ \args :: AttrSet (InferT s m (Judgment s))
args b :: 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

    (args :: AttrSet (InferT s m (Judgment s))
args, Judgment as :: Assumption
as cs :: [Constraint]
cs t :: 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 (\(_, TVar a :: 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 _ = 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 _ = String -> InferT s m NixString
forall a. HasCallStack => String -> a
error "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 _ _ (TSet _ xs :: AttrSet Type
xs)) = do
    let sing :: p -> Type -> Judgment s
sing _ = 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 _ = 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 v :: (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
    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 (xs :: AttrSet (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 -> 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 x :: Judgment s
x rest :: 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
$ \x' :: 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 xs :: [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 x :: Judgment s
x rest :: 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
$ \x' :: 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 _ = 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 []                = Env -> Either InferError Env
forall a b. b -> Either a b
Right Env
env
inferTop env :: Env
env ((name :: Name
name, ex :: NExpr
ex) : xs :: [(Name, NExpr)]
xs) = case Env -> NExpr -> Either InferError [Scheme]
inferExpr Env
env NExpr
ex of
  Left  err :: InferError
err -> InferError -> Either InferError Env
forall a b. a -> Either a b
Left InferError
err
  Right ty :: [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 _ body :: 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 a :: TVar
a  ) = [TVar
a]
  fv (a :: Type
a :~> b :: Type
b ) = Type -> [TVar]
fv Type
a [TVar] -> [TVar] -> [TVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TVar]
fv Type
b
  fv (TCon _  ) = []
  fv (TSet _ a :: 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 a :: [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 ts :: [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 (a :: Type
a :~> b :: Type
b ) = Type -> Type
normtype Type
a Type -> Type -> Type
:~> Type -> Type
normtype Type
b
  normtype (TCon a :: String
a  ) = String -> Type
TCon String
a
  normtype (TSet b :: Bool
b a :: 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 a :: [Type]
a ) = [Type] -> Type
TList ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
normtype [Type]
a)
  normtype (TMany ts :: [Type]
ts) = [Type] -> Type
TMany ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
normtype [Type]
ts)
  normtype (TVar  a :: 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 x :: TVar
x  -> TVar -> Type
TVar TVar
x
    Nothing -> String -> Type
forall a. HasCallStack => String -> a
error "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 err :: 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 _ _ = String -> Solver m a
forall a. HasCallStack => String -> a
error "This is never used"

runSolver :: Monad m => Solver m a -> m (Either [TypeError] [a])
runSolver :: Solver m a -> m (Either [TypeError] [a])
runSolver (Solver s :: 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
    (x :: a
x : xs :: [a]
xs, _ ) -> [a] -> Either [TypeError] [a]
forall a b. b -> Either a b
Right (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
    (_     , es :: [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 s1 :: Map TVar Type
s1 compose :: Subst -> Subst -> Subst
`compose` Subst s2 :: 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 (t1 :: Type
t1 : ts1 :: [Type]
ts1) (t2 :: Type
t2 : ts2 :: [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 t1 :: [Type]
t1 t2 :: [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 [_         ] = Bool
True
allSameType (x :: Type
x : y :: Type
y : ys :: [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 t1 :: Type
t1 t2 :: 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 v :: TVar
v) t :: Type
t        = TVar
v TVar -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
`bind` Type
t
unifies t :: Type
t        (TVar v :: TVar
v) = TVar
v TVar -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => TVar -> Type -> Solver m Subst
`bind` Type
t
unifies (TList xs :: [Type]
xs) (TList ys :: [Type]
ys)
  | [Type] -> Bool
allSameType [Type]
xs Bool -> Bool -> Bool
&& [Type] -> Bool
allSameType [Type]
ys = case ([Type]
xs, [Type]
ys) of
    (x :: Type
x : _, y :: Type
y : _) -> Type -> Type -> Solver m Subst
forall (m :: * -> *). Monad m => Type -> Type -> Solver m Subst
unifies Type
x Type
y
    _              -> 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 _    ) t2 :: Type
t2@(TList _    ) = 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 True _) (   TSet True _) = Subst -> Solver m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifies (TSet False b :: AttrSet Type
b) (TSet True s :: 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 True s :: AttrSet Type
s) (TSet False b :: 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 False s :: AttrSet Type
s) (TSet False b :: 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 (t1 :: Type
t1 :~> t2 :: Type
t2) (t3 :: Type
t3 :~> t4 :: 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 t1s :: [Type]
t1s) t2 :: 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 t1 :: Type
t1          (TMany t2s :: [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 t1 :: Type
t1          t2 :: 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 a :: TVar
a t :: 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 a :: TVar
a t :: 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 xs :: [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 xs :: [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{}     , _) = Bool
True
  solvable (ExpInstConst{}, _) = Bool
True
  solvable (ImpInstConst _t1 :: Type
_t1 ms :: Set TVar
ms t2 :: Type
t2, cs :: 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 xs :: [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
$ \c :: a -> StateT [TypeError] m r -> StateT [TypeError] m r
c n :: 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 cs :: [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 t1 :: Type
t1 t2 :: Type
t2, cs :: [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
>>- \su1 :: 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
>>- \su2 :: 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 t1 :: Type
t1 ms :: Set TVar
ms t2 :: Type
t2, cs :: [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 t :: Type
t s :: Scheme
s, cs :: [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