{-# 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           Nix.Thunk
-- import           Nix.Thunk.Basic
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) => 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