{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
module Jikka.Core.Language.TypeCheck where
import Jikka.Common.Error
import Jikka.Core.Format (formatExpr, formatType)
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Util
builtinToType :: Builtin -> Type
builtinToType :: Builtin -> Type
builtinToType = \case
Builtin
Negate -> Type -> Type
Fun1STy Type
IntTy
Builtin
Plus -> Type -> Type
Fun2STy Type
IntTy
Builtin
Minus -> Type -> Type
Fun2STy Type
IntTy
Builtin
Mult -> Type -> Type
Fun2STy Type
IntTy
Builtin
FloorDiv -> Type -> Type
Fun2STy Type
IntTy
Builtin
FloorMod -> Type -> Type
Fun2STy Type
IntTy
Builtin
CeilDiv -> Type -> Type
Fun2STy Type
IntTy
Builtin
CeilMod -> Type -> Type
Fun2STy Type
IntTy
Builtin
Pow -> Type -> Type
Fun2STy Type
IntTy
Builtin
Abs -> Type -> Type
Fun1STy Type
IntTy
Builtin
Gcd -> Type -> Type
Fun2STy Type
IntTy
Builtin
Lcm -> Type -> Type
Fun2STy Type
IntTy
Min2 Type
t -> Type -> Type
Fun2STy Type
t
Max2 Type
t -> Type -> Type
Fun2STy Type
t
Iterate Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
IntTy (Type -> Type -> Type
FunTy Type
t Type
t) Type
t Type
t
Builtin
Not -> Type -> Type
Fun1STy Type
BoolTy
Builtin
And -> Type -> Type
Fun2STy Type
BoolTy
Builtin
Or -> Type -> Type
Fun2STy Type
BoolTy
Builtin
Implies -> Type -> Type
Fun2STy Type
BoolTy
If Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
BoolTy Type
t Type
t Type
t
Builtin
BitNot -> Type -> Type
Fun1STy Type
IntTy
Builtin
BitAnd -> Type -> Type
Fun2STy Type
IntTy
Builtin
BitOr -> Type -> Type
Fun2STy Type
IntTy
Builtin
BitXor -> Type -> Type
Fun2STy Type
IntTy
Builtin
BitLeftShift -> Type -> Type
Fun2STy Type
IntTy
Builtin
BitRightShift -> Type -> Type
Fun2STy Type
IntTy
MatAp Int
h Int
w -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Int -> Type
matrixTy Int
h Int
w) (Int -> Type
vectorTy Int
w) (Int -> Type
vectorTy Int
h)
MatZero Int
n -> Int -> Int -> Type
matrixTy Int
n Int
n
MatOne Int
n -> Int -> Int -> Type
matrixTy Int
n Int
n
MatAdd Int
h Int
w -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Int -> Type
matrixTy Int
h Int
w) (Int -> Int -> Type
matrixTy Int
h Int
w) (Int -> Int -> Type
matrixTy Int
h Int
w)
MatMul Int
h Int
n Int
w -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Int -> Type
matrixTy Int
h Int
n) (Int -> Int -> Type
matrixTy Int
n Int
w) (Int -> Int -> Type
matrixTy Int
h Int
w)
MatPow Int
n -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Int -> Type
matrixTy Int
n Int
n) Type
IntTy (Int -> Int -> Type
matrixTy Int
n Int
n)
VecFloorMod Int
n -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Type
vectorTy Int
n) Type
IntTy (Int -> Type
vectorTy Int
n)
MatFloorMod Int
h Int
w -> Type -> Type -> Type -> Type
Fun2Ty (Int -> Int -> Type
matrixTy Int
h Int
w) Type
IntTy (Int -> Int -> Type
matrixTy Int
h Int
w)
Builtin
ModNegate -> Type -> Type
Fun2STy Type
IntTy
Builtin
ModPlus -> Type -> Type
Fun3STy Type
IntTy
Builtin
ModMinus -> Type -> Type
Fun3STy Type
IntTy
Builtin
ModMult -> Type -> Type
Fun3STy Type
IntTy
Builtin
ModInv -> Type -> Type
Fun2STy Type
IntTy
Builtin
ModPow -> Type -> Type
Fun3STy Type
IntTy
ModMatAp Int
h Int
w -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Int -> Int -> Type
matrixTy Int
h Int
w) (Int -> Type
vectorTy Int
w) Type
IntTy (Int -> Type
vectorTy Int
h)
ModMatAdd Int
h Int
w -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Int -> Int -> Type
matrixTy Int
h Int
w) (Int -> Int -> Type
matrixTy Int
h Int
w) Type
IntTy (Int -> Int -> Type
matrixTy Int
h Int
w)
ModMatMul Int
h Int
n Int
w -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Int -> Int -> Type
matrixTy Int
h Int
n) (Int -> Int -> Type
matrixTy Int
n Int
w) Type
IntTy (Int -> Int -> Type
matrixTy Int
h Int
w)
ModMatPow Int
n -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Int -> Int -> Type
matrixTy Int
n Int
n) Type
IntTy Type
IntTy (Int -> Int -> Type
matrixTy Int
n Int
n)
Cons Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t (Type -> Type
ListTy Type
t) (Type -> Type
ListTy Type
t)
Snoc Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
t) Type
t (Type -> Type
ListTy Type
t)
Foldl Type
t1 Type
t2 -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type -> Type
Fun2Ty Type
t2 Type
t1 Type
t2) Type
t2 (Type -> Type
ListTy Type
t1) Type
t2
Scanl Type
t1 Type
t2 -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type -> Type
Fun2Ty Type
t2 Type
t1 Type
t2) Type
t2 (Type -> Type
ListTy Type
t1) (Type -> Type
ListTy Type
t2)
Build Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
t) (Type -> Type
ListTy Type
t) Type
IntTy (Type -> Type
ListTy Type
t)
Len Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
Map Type
t1 Type
t2 -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type -> Type
FunTy Type
t1 Type
t2) (Type -> Type
ListTy Type
t1) (Type -> Type
ListTy Type
t2)
Filter Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type -> Type
FunTy Type
t Type
BoolTy) (Type -> Type
ListTy Type
t) (Type -> Type
ListTy Type
t)
At Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
t) Type
IntTy Type
t
SetAt Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type
ListTy Type
t) Type
IntTy Type
t (Type -> Type
ListTy Type
t)
Elem Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t (Type -> Type
ListTy Type
t) Type
BoolTy
Builtin
Sum -> Type -> Type
FunLTy Type
IntTy
Builtin
Product -> Type -> Type
FunLTy Type
IntTy
Builtin
ModSum -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
IntTy) Type
IntTy Type
IntTy
Builtin
ModProduct -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
IntTy) Type
IntTy Type
IntTy
Min1 Type
t -> Type -> Type
FunLTy Type
t
Max1 Type
t -> Type -> Type
FunLTy Type
t
ArgMin Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
ArgMax Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
Builtin
All -> Type -> Type
FunLTy Type
BoolTy
Builtin
Any -> Type -> Type
FunLTy Type
BoolTy
Sorted Type
t -> Type -> Type
Fun1STy (Type -> Type
ListTy Type
t)
Reversed Type
t -> Type -> Type
Fun1STy (Type -> Type
ListTy Type
t)
Builtin
Range1 -> Type -> Type -> Type
FunTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
Builtin
Range2 -> Type -> Type -> Type -> Type
Fun2Ty Type
IntTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
Builtin
Range3 -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
IntTy Type
IntTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
Tuple [Type]
ts -> [Type] -> Type -> Type
curryFunTy [Type]
ts ([Type] -> Type
TupleTy [Type]
ts)
Proj [Type]
ts Int
n -> Type -> Type -> Type
FunTy ([Type] -> Type
TupleTy [Type]
ts) ([Type]
ts [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! Int
n)
LessThan Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
LessEqual Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
GreaterThan Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
GreaterEqual Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
Equal Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
NotEqual Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
Builtin
Fact -> Type -> Type
Fun1STy Type
IntTy
Builtin
Choose -> Type -> Type
Fun2STy Type
IntTy
Builtin
Permute -> Type -> Type
Fun2STy Type
IntTy
Builtin
MultiChoose -> Type -> Type
Fun2STy Type
IntTy
Builtin
ConvexHullTrickInit -> Type
ConvexHullTrickTy
Builtin
ConvexHullTrickGetMin -> Type -> Type -> Type -> Type
Fun2Ty Type
ConvexHullTrickTy Type
IntTy Type
IntTy
Builtin
ConvexHullTrickInsert -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
ConvexHullTrickTy Type
IntTy Type
IntTy Type
ConvexHullTrickTy
SegmentTreeInitList Semigroup'
semigrp -> Type -> Type -> Type
FunTy (Type -> Type
ListTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp)) (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp)
SegmentTreeGetRange Semigroup'
semigrp -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp) Type
IntTy Type
IntTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp)
SegmentTreeSetPoint Semigroup'
semigrp -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp) Type
IntTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp) (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp)
semigroupToType :: Semigroup' -> Type
semigroupToType :: Semigroup' -> Type
semigroupToType = \case
Semigroup'
SemigroupIntPlus -> Type
IntTy
Semigroup'
SemigroupIntMin -> Type
IntTy
Semigroup'
SemigroupIntMax -> Type
IntTy
literalToType :: Literal -> Type
literalToType :: Literal -> Type
literalToType = \case
LitBuiltin Builtin
builtin -> Builtin -> Type
builtinToType Builtin
builtin
LitInt Integer
_ -> Type
IntTy
LitBool Bool
_ -> Type
BoolTy
LitNil Type
t -> Type -> Type
ListTy Type
t
LitBottom Type
t String
_ -> Type
t
arityOfBuiltin :: Builtin -> Int
arityOfBuiltin :: Builtin -> Int
arityOfBuiltin = \case
Min2 Type
_ -> Int
2
Max2 Type
_ -> Int
2
Foldl Type
_ Type
_ -> Int
3
Iterate Type
_ -> Int
3
At Type
_ -> Int
2
Min1 Type
_ -> Int
1
Max1 Type
_ -> Int
1
Proj [Type]
_ Int
_ -> Int
1
Builtin
builtin -> [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Type], Type) -> [Type]
forall a b. (a, b) -> a
fst (Type -> ([Type], Type)
uncurryFunTy (Builtin -> Type
builtinToType Builtin
builtin)))
type TypeEnv = [(VarName, Type)]
typecheckExpr :: MonadError Error m => TypeEnv -> Expr -> m Type
typecheckExpr :: TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env = \case
Var VarName
x -> case VarName -> TypeEnv -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarName
x TypeEnv
env of
Maybe Type
Nothing -> String -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ String
"undefined variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
unVarName VarName
x
Just Type
t -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
Lit Literal
lit -> 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
$ Literal -> Type
literalToType Literal
lit
App Expr
f Expr
e -> do
Type
tf <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
f
Type
te <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
case Type
tf of
FunTy Type
te' Type
ret | Type
te' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
te -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ret
Type
_ -> String -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ String
"wrong type funcall: function = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and argument = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", function's type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
tf String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but argument's type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
te
Lam VarName
x Type
t Expr
e -> Type -> Type -> Type
FunTy Type
t (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr ((VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) Expr
e
Let VarName
x Type
t Expr
e1 Expr
e2 -> do
Type
t' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e1
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"wrong type binding: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr (VarName -> Type -> Expr -> Expr -> Expr
Let VarName
x Type
t Expr
e1 Expr
e2)
TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr ((VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) Expr
e2
typecheckToplevelExpr :: MonadError Error m => TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr :: TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr TypeEnv
env = \case
ResultExpr Expr
e -> TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
ToplevelLet VarName
x Type
t Expr
e ToplevelExpr
cont -> do
Type
t' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"assigned type is not correct: context = (let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
unVarName VarName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in ...), expected type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", actual type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t'
TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr ((VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) ToplevelExpr
cont
ToplevelLetRec VarName
f TypeEnv
args Type
ret Expr
body ToplevelExpr
cont -> do
let t :: Type
t = case TypeEnv
args of
[] -> Type
ret
TypeEnv
_ -> [Type] -> Type -> Type
curryFunTy (((VarName, Type) -> Type) -> TypeEnv -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (VarName, Type) -> Type
forall a b. (a, b) -> b
snd TypeEnv
args) Type
ret
Type
ret' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr (TypeEnv -> TypeEnv
forall a. [a] -> [a]
reverse TypeEnv
args TypeEnv -> TypeEnv -> TypeEnv
forall a. [a] -> [a] -> [a]
++ (VarName
f, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) Expr
body
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
ret' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ret) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"returned type is not correct: context = (let rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
unVarName VarName
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((VarName, Type) -> String) -> TypeEnv -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(VarName
x, Type
t) -> VarName -> String
unVarName VarName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t) TypeEnv
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
body String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in ...), expected type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", actual type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret'
TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr ((VarName
f, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) ToplevelExpr
cont
typecheckProgram :: MonadError Error m => Program -> m Type
typecheckProgram :: ToplevelExpr -> m Type
typecheckProgram ToplevelExpr
prog = String -> m Type -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a -> m a
wrapError' String
"Jikka.Core.Language.TypeCheck.typecheckProgram" (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ do
TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr [] ToplevelExpr
prog