{-# LANGUAGE TupleSections #-}

module TypeChecker.TypeChecker (inferProgram, checkProgram) where

import Control.Category ((>>>))
import Control.Monad.Except
import Control.Monad.Reader
import Control.Unification.IntVar (evalIntBindingT)
import Data.Either.Extra (mapRight)
import Data.Functor.Identity (Identity (runIdentity))
import Data.List.NonEmpty (toList)
import qualified Data.Map as M
import Data.Maybe
import Parser.Ast
import qualified StdLib
import Trees.Common
import qualified Trees.Common as L
import TypeChecker.HindleyMilner
import Prelude hiding (lookup)

-- * Program Type Checker

checkProgram :: Program -> Either TypeError ()
checkProgram :: Program -> Either TypeError ()
checkProgram = (Polytype -> ())
-> Either TypeError Polytype -> Either TypeError ()
forall b c a. (b -> c) -> Either a b -> Either a c
mapRight (() -> Polytype -> ()
forall a b. a -> b -> a
const ()) (Either TypeError Polytype -> Either TypeError ())
-> (Program -> Either TypeError Polytype)
-> Program
-> Either TypeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program -> Either TypeError Polytype
inferProgram

inferProgram :: Program -> Either TypeError Polytype
inferProgram :: Program -> Either TypeError Polytype
inferProgram (Program [Statement]
stmts) = Infer UType -> Either TypeError Polytype
runInfer (Infer UType -> Either TypeError Polytype)
-> Infer UType -> Either TypeError Polytype
forall a b. (a -> b) -> a -> b
$ Infer UType -> Infer UType
forall {b}.
ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
withStdLib ([Statement] -> Infer UType
inferStatements [Statement]
stmts)
  where
    runInfer :: Infer UType -> Either TypeError Polytype
    runInfer :: Infer UType -> Either TypeError Polytype
runInfer =
      (Infer UType -> (UType -> Infer UType) -> Infer UType
forall a b.
ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
-> (a
    -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b)
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UType -> Infer UType
applyBindings)
        (Infer UType -> Infer UType)
-> (Infer UType -> Either TypeError Polytype)
-> Infer UType
-> Either TypeError Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (Infer UType
-> (UType
    -> ReaderT
         Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype)
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
forall a b.
ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
-> (a
    -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b)
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UType -> Infer UPolytype
generalize (UType -> Infer UPolytype)
-> (Infer UPolytype
    -> ReaderT
         Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype)
-> UType
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (UPolytype -> Polytype)
-> Infer UPolytype
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
forall a b.
(a -> b)
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UPolytype -> Polytype
toPolytype))
        (Infer UType
 -> ReaderT
      Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype)
-> (ReaderT
      Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
    -> Either TypeError Polytype)
-> Infer UType
-> Either TypeError Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (ReaderT
   Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
 -> Ctx -> ExceptT TypeError (IntBindingT TypeF Identity) Polytype)
-> Ctx
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
-> ExceptT TypeError (IntBindingT TypeF Identity) Polytype
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
-> Ctx -> ExceptT TypeError (IntBindingT TypeF Identity) Polytype
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Ctx
forall k a. Map k a
M.empty
        (ReaderT
   Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
 -> ExceptT TypeError (IntBindingT TypeF Identity) Polytype)
-> (ExceptT TypeError (IntBindingT TypeF Identity) Polytype
    -> Either TypeError Polytype)
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Polytype
-> Either TypeError Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ExceptT TypeError (IntBindingT TypeF Identity) Polytype
-> IntBindingT TypeF Identity (Either TypeError Polytype)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
        (ExceptT TypeError (IntBindingT TypeF Identity) Polytype
 -> IntBindingT TypeF Identity (Either TypeError Polytype))
-> (IntBindingT TypeF Identity (Either TypeError Polytype)
    -> Either TypeError Polytype)
-> ExceptT TypeError (IntBindingT TypeF Identity) Polytype
-> Either TypeError Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> IntBindingT TypeF Identity (Either TypeError Polytype)
-> Identity (Either TypeError Polytype)
forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT
        (IntBindingT TypeF Identity (Either TypeError Polytype)
 -> Identity (Either TypeError Polytype))
-> (Identity (Either TypeError Polytype)
    -> Either TypeError Polytype)
-> IntBindingT TypeF Identity (Either TypeError Polytype)
-> Either TypeError Polytype
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Identity (Either TypeError Polytype) -> Either TypeError Polytype
forall a. Identity a -> a
runIdentity

    withStdLib :: ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
withStdLib ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
infer = do
      let generalizeDecl :: (t, Type)
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) (t, UPolytype)
generalizeDecl (t
ident, Type
t) = (t
ident,) (UPolytype -> (t, UPolytype))
-> Infer UPolytype
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) (t, UPolytype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UType -> Infer UPolytype
generalize (Type -> UType
toUType Type
t)
      [(Identifier, UPolytype)]
generalizedDecls <- ((Identifier, Type)
 -> ReaderT
      Ctx
      (ExceptT TypeError (IntBindingT TypeF Identity))
      (Identifier, UPolytype))
-> [(Identifier, Type)]
-> ReaderT
     Ctx
     (ExceptT TypeError (IntBindingT TypeF Identity))
     [(Identifier, UPolytype)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Identifier, Type)
-> ReaderT
     Ctx
     (ExceptT TypeError (IntBindingT TypeF Identity))
     (Identifier, UPolytype)
forall {t}.
(t, Type)
-> ReaderT
     Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) (t, UPolytype)
generalizeDecl [(Identifier, Type)]
StdLib.typedDecls
      (Ctx -> Ctx)
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
forall a.
(Ctx -> Ctx)
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Ctx -> Ctx -> Ctx
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union ([(Identifier, UPolytype)] -> Ctx
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Identifier, UPolytype)]
generalizedDecls)) ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) b
infer

-- * Internal

inferStatements :: [Statement] -> Infer UType
inferStatements :: [Statement] -> Infer UType
inferStatements [Statement]
x = [Statement] -> Infer UType -> Infer UType
inferStatements' [Statement]
x (TypeError -> Infer UType
forall a.
TypeError
-> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeError
Unreachable)

inferStatements' :: [Statement] -> Infer UType -> Infer UType
inferStatements' :: [Statement] -> Infer UType -> Infer UType
inferStatements' [] Infer UType
t = Infer UType
t
inferStatements' ((StmtExpr Expression
e) : [Statement]
stmts) Infer UType
_ = do
  UType
res <- Expression -> Infer UType
inferExpr Expression
e
  [Statement] -> Infer UType -> Infer UType
inferStatements' [Statement]
stmts (UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
res)
inferStatements' ((StmtDecl (DeclVar (Identifier
ident, Maybe Type
t) Expression
val)) : [Statement]
stmts) Infer UType
_ = do
  UType
t' <- Expression -> Infer UType
inferExpr Expression
val
  UType
t'' <- UType -> Maybe Type -> Infer UType
checkByAnnotation UType
t' Maybe Type
t
  UPolytype
upt <- UType -> Infer UPolytype
generalize UType
t''
  Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident UPolytype
upt (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ [Statement] -> Infer UType -> Infer UType
inferStatements' [Statement]
stmts (UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
t'')
inferStatements' ((StmtDecl (DeclFun Identifier
ident IsRec
isRec Fun
fun)) : [Statement]
stmts) Infer UType
_ = do
  UType
funT <-
    if IsRec
isRec
      then do
        UType
funT <- Infer UType
fresh
        UType
funT' <- Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident ([Identifier] -> UType -> UPolytype
forall t. [Identifier] -> t -> Poly t
Forall [] UType
funT) (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Fun -> Infer UType
inferFun Fun
fun
        Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident ([Identifier] -> UType -> UPolytype
forall t. [Identifier] -> t -> Poly t
Forall [] UType
funT') (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Fun -> Infer UType
inferFun Fun
fun
      else Fun -> Infer UType
inferFun Fun
fun
  UPolytype
funUT <- UType -> Infer UPolytype
generalize UType
funT
  Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident UPolytype
funUT (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ [Statement] -> Infer UType -> Infer UType
inferStatements' [Statement]
stmts (UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
funT)

inferExpr :: Expression -> Infer UType
inferExpr :: Expression -> Infer UType
inferExpr (ExprId Identifier
ident) = Identifier -> Infer UType
lookup Identifier
ident
inferExpr (ExprPrimVal PrimitiveValue
value) = case PrimitiveValue
value of
  PrimitiveValue
PrimValUnit -> UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTUnit
  PrimValBool IsRec
_ -> UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTBool
  PrimValInt Int64
_ -> UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTInt
inferExpr (ExprBinOp BinaryOperator
op Expression
lhs Expression
rhs) = do
  UType
lhsT <- Expression -> Infer UType
inferExpr Expression
lhs
  UType
rhsT <- Expression -> Infer UType
inferExpr Expression
rhs
  (TypeError -> TypeError) -> Infer UType -> Infer UType
forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
withError (TypeError -> TypeError -> TypeError
forall a b. a -> b -> a
const (TypeError -> TypeError -> TypeError)
-> TypeError -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ UType -> UType -> TypeError
ImpossibleBinOpApplication UType
lhsT UType
rhsT) (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ do
    UType
valT <- UType
lhsT UType -> UType -> Infer UType
=:= UType
rhsT
    case BinaryOperator
op of
      BoolOp BooleanOperator
_ -> UType
valT UType -> UType -> Infer UType
=:= UType
UTBool
      ArithOp ArithmeticOperator
_ -> UType
valT UType -> UType -> Infer UType
=:= UType
UTInt
      CompOp ComparisonOperator
_ -> UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTBool
inferExpr (ExprUnOp UnaryOperator
op Expression
val) = do
  UType
valT <- Expression -> Infer UType
inferExpr Expression
val
  (TypeError -> TypeError) -> Infer UType -> Infer UType
forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
withError (TypeError -> TypeError -> TypeError
forall a b. a -> b -> a
const (TypeError -> TypeError -> TypeError)
-> TypeError -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ UType -> TypeError
ImpossibleUnOpApplication UType
valT) (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ case UnaryOperator
op of
    UnaryOperator
UnMinusOp -> UType
valT UType -> UType -> Infer UType
=:= UType
UTInt
inferExpr (ExprApp Expression
funExpr Expression
argExpr) = do
  UType
funT <- Expression -> Infer UType
inferExpr Expression
funExpr
  UType
argT <- Expression -> Infer UType
inferExpr Expression
argExpr
  UType
resT <- Infer UType
fresh
  UType
_ <- UType
funT UType -> UType -> Infer UType
=:= UType -> UType -> UType
UTFun UType
argT UType
resT
  UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
resT
inferExpr (ExprIte Expression
c Expression
t Expression
e) = do
  UType
_ <- Expression -> UType -> Infer UType
check Expression
c UType
UTBool
  UType
tT <- Expression -> Infer UType
inferExpr Expression
t
  UType
eT <- Expression -> Infer UType
inferExpr Expression
e
  UType
tT UType -> UType -> Infer UType
=:= UType
eT
inferExpr (ExprLetIn Declaration
decl Expression
expr) = Declaration -> Expression -> Infer UType
inferLetIn Declaration
decl Expression
expr
inferExpr (ExprFun Fun
fun) = Fun -> Infer UType
inferFun Fun
fun

inferLetIn :: Declaration -> Expression -> Infer UType
inferLetIn :: Declaration -> Expression -> Infer UType
inferLetIn (DeclVar (Identifier
ident, Maybe Type
t) Expression
val) Expression
expr = do
  UType
t' <- Expression -> Infer UType
inferExpr Expression
val
  UType
t'' <- UType -> Maybe Type -> Infer UType
checkByAnnotation UType
t' Maybe Type
t
  UPolytype
upt <- UType -> Infer UPolytype
generalize UType
t''
  Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident UPolytype
upt (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Expression -> Infer UType
inferExpr Expression
expr
inferLetIn (DeclFun Identifier
ident IsRec
isRec Fun
fun) Expression
expr = do
  UType
funT <-
    if IsRec
isRec
      then do
        UType
funT <- Infer UType
fresh
        UType
funT' <- Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident ([Identifier] -> UType -> UPolytype
forall t. [Identifier] -> t -> Poly t
Forall [] UType
funT) (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Fun -> Infer UType
inferFun Fun
fun
        Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident ([Identifier] -> UType -> UPolytype
forall t. [Identifier] -> t -> Poly t
Forall [] UType
funT') (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Fun -> Infer UType
inferFun Fun
fun
      else Fun -> Infer UType
inferFun Fun
fun
  UPolytype
funUT <- UType -> Infer UPolytype
generalize UType
funT
  Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident UPolytype
funUT (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ Expression -> Infer UType
inferExpr Expression
expr

inferFun :: Fun -> Infer UType
inferFun :: Fun -> Infer UType
inferFun (Fun NonEmpty (Identifier, Maybe Type)
params Maybe Type
resT Expression
body) = [(Identifier, Maybe Type)] -> Infer UType
inferFun' ([(Identifier, Maybe Type)] -> Infer UType)
-> [(Identifier, Maybe Type)] -> Infer UType
forall a b. (a -> b) -> a -> b
$ NonEmpty (Identifier, Maybe Type) -> [(Identifier, Maybe Type)]
forall a. NonEmpty a -> [a]
toList NonEmpty (Identifier, Maybe Type)
params
  where
    inferFun' :: [(Identifier, Maybe Type)] -> Infer UType
inferFun' [(Identifier, Maybe Type)]
params' = case [(Identifier, Maybe Type)]
params' of
      [] -> do
        UType
bodyT <- Expression -> Infer UType
inferExpr Expression
body
        UType -> Maybe Type -> Infer UType
checkByAnnotation UType
bodyT Maybe Type
resT
      (Identifier
ident, Maybe Type
t) : [(Identifier, Maybe Type)]
params'' -> do
        UType
t' <- Infer UType -> (Type -> Infer UType) -> Maybe Type -> Infer UType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Infer UType
fresh (UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UType -> Infer UType) -> (Type -> UType) -> Type -> Infer UType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> UType
toUType) Maybe Type
t
        Identifier -> UPolytype -> Infer UType -> Infer UType
forall (m :: * -> *) a.
MonadReader Ctx m =>
Identifier -> UPolytype -> m a -> m a
withBinding Identifier
ident ([Identifier] -> UType -> UPolytype
forall t. [Identifier] -> t -> Poly t
Forall [] UType
t') (Infer UType -> Infer UType) -> Infer UType -> Infer UType
forall a b. (a -> b) -> a -> b
$ UType -> UType -> UType
UTFun UType
t' (UType -> UType) -> Infer UType -> Infer UType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Identifier, Maybe Type)] -> Infer UType
inferFun' [(Identifier, Maybe Type)]
params''

-- ** Utils

check :: Expression -> UType -> Infer UType
check :: Expression -> UType -> Infer UType
check Expression
expr UType
t = do
  UType
exprT <- Expression -> Infer UType
inferExpr Expression
expr
  UType
t UType -> UType -> Infer UType
=:= UType
exprT

checkByAnnotation :: UType -> Maybe L.Type -> Infer UType
checkByAnnotation :: UType -> Maybe Type -> Infer UType
checkByAnnotation UType
t Maybe Type
ann = case Maybe Type
ann of
  Just Type
annT -> Type -> UType
toUType Type
annT UType -> UType -> Infer UType
=:= UType
t
  Maybe Type
Nothing -> UType -> Infer UType
forall a.
a -> ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
t