{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      : Jikka.Core.Language.RewriteRules
-- Description : checks and obtains types of exprs. / 式の型を検査し取得します。
-- Copyright   : (c) Kimiyuki Onaka, 2021
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
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
  -- arithmetical functions
  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
  -- advanced arithmetical functions
  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
  -- logical functions
  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
  -- bitwise functions
  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
  -- matrix functions
  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)
  -- modular functions
  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)
  -- list functions
  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 functions
  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)
  -- comparison
  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
  -- combinational functions
  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
  -- data structure
  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` checks that the given `Expr` has the correct types.
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