-- |
-- Module      :  Cryptol.TypeCheck.Sanity
-- Copyright   :  (c) 2015-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Sanity
  ( tcExpr
  , tcDecls
  , tcModule
  , ProofObligation
  , onlyNonTrivial
  , Error(..)
  , AreSame(..)
  , same
  ) where


import Data.Maybe(maybeToList)
import Data.List (sort)
import qualified Data.Set as Set
import MonadLib
import qualified Control.Applicative as A
import           Data.Map ( Map )
import qualified Data.Map as Map

import Cryptol.Parser.Position(thing,Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst, mergeDistinctSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.ModuleSystem.Name(nameLoc,nameIdent)
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
import Cryptol.Utils.PP


tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [ ProofObligation ])
tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [Schema])
tcExpr InferInput
env Expr
e = InferInput
-> TcM Schema -> Either (Range, Error) (Schema, [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env (Expr -> TcM Schema
exprSchema Expr
e)

tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [ ProofObligation ]
tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [Schema]
tcDecls InferInput
env [DeclGroup]
ds0 = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env ([DeclGroup] -> TcM ()
checkDecls [DeclGroup]
ds0) of
                    Left (Range, Error)
err     -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
                    Right (()
_,[Schema]
ps) -> [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right [Schema]
ps

tcModule :: InferInput -> Module -> Either (Range, Error) [ ProofObligation ]
tcModule :: InferInput -> Module -> Either (Range, Error) [Schema]
tcModule InferInput
env Module
m = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env TcM ()
check of
                   Left (Range, Error)
err -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
                   Right (()
_,[Schema]
ps) -> [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right [Schema]
ps
  where check :: TcM ()
check = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> TcM () -> TcM ()
forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
k1 ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (Module -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes Module
m)))
        k1 :: TcM ()
k1    = (Type -> TcM () -> TcM ()) -> TcM () -> [Type] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> TcM () -> TcM ()
forall a. Type -> TcM a -> TcM a
withAsmp TcM ()
k2 ((Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing (Module -> [Located Type]
forall mname. ModuleG mname -> [Located Type]
mParamConstraints Module
m))
        k2 :: TcM ()
k2    = [(Name, Schema)] -> TcM () -> TcM ()
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars (Map Name Schema -> [(Name, Schema)]
forall k a. Map k a -> [(k, a)]
Map.toList ((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (Module -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns Module
m)))
              (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ [(Name, Schema)] -> TcM () -> TcM ()
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars ((NominalType -> [(Name, Schema)])
-> [NominalType] -> [(Name, Schema)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NominalType -> [(Name, Schema)]
nominalTypeConTypes
                                                (Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (Module -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes Module
m)))
              (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> TcM ()
checkDecls (Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m)

onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
onlyNonTrivial :: [Schema] -> [Schema]
onlyNonTrivial = (Schema -> Bool) -> [Schema] -> [Schema]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Schema -> Bool) -> Schema -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Schema -> Bool
trivialProofObligation)

-- | Identify proof obligations that are obviously true.
-- We can filter these to avoid clutter
trivialProofObligation :: ProofObligation -> Bool
trivialProofObligation :: Schema -> Bool
trivialProofObligation Schema
oblig = Type -> Bool
pIsTrue Type
goal Bool -> Bool -> Bool
|| Bool
simpleEq Bool -> Bool -> Bool
|| Type
goal Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
asmps
  where
  goal :: Type
goal  = Schema -> Type
sType Schema
oblig
  asmps :: [Type]
asmps = Schema -> [Type]
sProps Schema
oblig
  simpleEq :: Bool
simpleEq = case Type -> Maybe (Type, Type)
pIsEqual Type
goal of
               Just (Type
t1,Type
t2) -> Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2
               Maybe (Type, Type)
Nothing      -> Bool
False


--------------------------------------------------------------------------------

checkDecls :: [DeclGroup] -> TcM ()
checkDecls :: [DeclGroup] -> TcM ()
checkDecls [DeclGroup]
decls =
  case [DeclGroup]
decls of
    [] -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    DeclGroup
d : [DeclGroup]
ds -> do [(Name, Schema)]
xs <- DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
d
                 [(Name, Schema)] -> TcM () -> TcM ()
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs ([DeclGroup] -> TcM ()
checkDecls [DeclGroup]
ds)

-- | Validate a type, returning its kind.
checkType :: Type -> TcM Kind
checkType :: Type -> TcM Kind
checkType Type
ty =
  case Type
ty of
    TUser Name
_ [Type]
_ Type
t -> Type -> TcM Kind
checkType Type
t    -- Maybe check synonym too?

    TCon TCon
tc [Type]
ts ->
      do [Kind]
ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
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 Type -> TcM Kind
checkType [Type]
ts
         Kind -> [Kind] -> TcM Kind
checkKind (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
tc) [Kind]
ks

    TNominal NominalType
nt [Type]
ts ->
      do [Kind]
ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
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 Type -> TcM Kind
checkType [Type]
ts
         Kind -> [Kind] -> TcM Kind
checkKind (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt) [Kind]
ks

    TVar TVar
tv -> TVar -> TcM Kind
lookupTVar TVar
tv

    TRec RecordMap Ident Type
fs ->
      do RecordMap Ident Type -> (Type -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RecordMap Ident Type
fs ((Type -> TcM ()) -> TcM ()) -> (Type -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Type
t ->
           do Kind
k <- Type -> TcM Kind
checkType Type
t
              Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KType) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
KType Kind
k
         Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
KType


  where
  checkKind :: Kind -> [Kind] -> TcM Kind
checkKind Kind
k [] = case Kind
k of
                     Kind
_ :-> Kind
_  -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Error
NotEnoughArgumentsInKind Kind
k
                     Kind
KProp    -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     Kind
KNum     -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     Kind
KType    -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k

  checkKind (Kind
k1 :-> Kind
k2) (Kind
k : [Kind]
ks)
    | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k1   = Kind -> [Kind] -> TcM Kind
checkKind Kind
k2 [Kind]
ks
    | Bool
otherwise = Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k

  checkKind Kind
k [Kind]
ks = Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> [Kind] -> Error
BadTypeApplication Kind
k [Kind]
ks


-- | Check that the type is valid, and it has the given kind.
checkTypeIs :: Kind -> Type -> TcM ()
checkTypeIs :: Kind -> Type -> TcM ()
checkTypeIs Kind
k Type
ty =
  do Kind
k1 <- Type -> TcM Kind
checkType Type
ty
     Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k1) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k Kind
k1

-- | Check that this is a valid schema.
checkSchema :: Schema -> TcM ()
checkSchema :: Schema -> TcM ()
checkSchema (Forall [TParam]
as [Type]
ps Type
t) = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> TcM () -> TcM ()
forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
check [TParam]
as
  where check :: TcM ()
check = do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Kind -> Type -> TcM ()
checkTypeIs Kind
KProp) [Type]
ps
                   Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t

data AreSame = SameIf [Prop]
             | NotSame

areSame :: AreSame
areSame :: AreSame
areSame = [Type] -> AreSame
SameIf []

sameAnd :: AreSame -> AreSame -> AreSame
sameAnd :: AreSame -> AreSame -> AreSame
sameAnd AreSame
x AreSame
y =
  case (AreSame
x,AreSame
y) of
    (SameIf [Type]
xs, SameIf [Type]
ys) -> [Type] -> AreSame
SameIf ([Type]
xs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ys)
    (AreSame, AreSame)
_                      -> AreSame
NotSame

sameBool :: Bool -> AreSame
sameBool :: Bool -> AreSame
sameBool Bool
b = if Bool
b then AreSame
areSame else AreSame
NotSame

sameTypes :: String -> Type -> Type -> TcM ()
sameTypes :: String -> Type -> Type -> TcM ()
sameTypes String
msg Type
x Type
y = String -> Schema -> Schema -> TcM ()
sameSchemas String
msg (Type -> Schema
tMono Type
x) (Type -> Schema
tMono Type
y)

sameSchemas :: String -> Schema -> Schema -> TcM ()
sameSchemas :: String -> Schema -> Schema -> TcM ()
sameSchemas String
msg Schema
x Schema
y =
  case Schema -> Schema -> AreSame
forall a. Same a => a -> a -> AreSame
same Schema
x Schema
y of
    AreSame
NotSame   -> Error -> TcM ()
forall a. Error -> TcM a
reportError (String -> Schema -> Schema -> Error
TypeMismatch String
msg Schema
x Schema
y)
    SameIf [Type]
ps -> (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps


class Same a where
  same :: a -> a -> AreSame

instance Same a => Same [a] where
  same :: [a] -> [a] -> AreSame
same [] [] = AreSame
areSame
  same (a
x : [a]
xs) (a
y : [a]
ys) = a -> a -> AreSame
forall a. Same a => a -> a -> AreSame
same a
x a
y AreSame -> AreSame -> AreSame
`sameAnd` [a] -> [a] -> AreSame
forall a. Same a => a -> a -> AreSame
same [a]
xs [a]
ys
  same [a]
_ [a]
_ = AreSame
NotSame

data Field a b = Field a b

instance (Eq a, Same b) => Same (Field a b) where
  same :: Field a b -> Field a b -> AreSame
same (Field a
x b
a) (Field a
y b
b) = Bool -> AreSame
sameBool (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y) AreSame -> AreSame -> AreSame
`sameAnd` b -> b -> AreSame
forall a. Same a => a -> a -> AreSame
same b
a b
b

instance Same Type where
  same :: Type -> Type -> AreSame
same Type
t1 Type
t2
    | Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
k2    = AreSame
NotSame
    | Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum  = if Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 then [Type] -> AreSame
SameIf [] else [Type] -> AreSame
SameIf [ Type
t1 Type -> Type -> Type
=#= Type
t2 ]
    | Bool
otherwise   =
      case (Type -> Type
tNoUser Type
t1, Type -> Type
tNoUser Type
t2) of
        (TVar TVar
x, TVar TVar
y)               -> Bool -> AreSame
sameBool (TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y)
        (TRec RecordMap Ident Type
x, TRec RecordMap Ident Type
y)               -> [Field Ident Type] -> [Field Ident Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (RecordMap Ident Type -> [Field Ident Type]
forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
x) (RecordMap Ident Type -> [Field Ident Type]
forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
y)
        (TNominal NominalType
x [Type]
xs, TNominal NominalType
y [Type]
ys) -> Field NominalType [Type] -> Field NominalType [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (NominalType -> [Type] -> Field NominalType [Type]
forall a b. a -> b -> Field a b
Field NominalType
x [Type]
xs) (NominalType -> [Type] -> Field NominalType [Type]
forall a b. a -> b -> Field a b
Field NominalType
y [Type]
ys)
        (TCon TCon
x [Type]
xs, TCon TCon
y [Type]
ys)         -> Field TCon [Type] -> Field TCon [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (TCon -> [Type] -> Field TCon [Type]
forall a b. a -> b -> Field a b
Field TCon
x [Type]
xs) (TCon -> [Type] -> Field TCon [Type]
forall a b. a -> b -> Field a b
Field TCon
y [Type]
ys)
        (Type, Type)
_                              -> AreSame
NotSame
      where
      k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
      k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2
      mkRec :: RecordMap a b -> [Field a b]
mkRec RecordMap a b
r = [ a -> b -> Field a b
forall a b. a -> b -> Field a b
Field a
x b
y | (a
x,b
y) <- RecordMap a b -> [(a, b)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap a b
r ]

instance Same Schema where
  same :: Schema -> Schema -> AreSame
same (Forall [TParam]
xs [Type]
ps Type
s) (Forall [TParam]
ys [Type]
qs Type
t) =
    [TParam] -> [TParam] -> AreSame
forall a. Same a => a -> a -> AreSame
same [TParam]
xs [TParam]
ys AreSame -> AreSame -> AreSame
`sameAnd` [Type] -> [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same [Type]
ps [Type]
qs AreSame -> AreSame -> AreSame
`sameAnd` Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
s Type
t

instance Same TParam where
  same :: TParam -> TParam -> AreSame
same TParam
x TParam
y = Bool -> AreSame
sameBool (TParam -> Maybe Name
tpName TParam
x Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Maybe Name
tpName TParam
y Bool -> Bool -> Bool
&& TParam -> Kind
tpKind TParam
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Kind
tpKind TParam
y)





--------------------------------------------------------------------------------


-- | Check that the expression is well-formed, and compute its type.
-- Reports an error if the expression is not of a mono type.
exprType :: Expr -> TcM Type
exprType :: Expr -> TcM Type
exprType Expr
expr =
  do Schema
s <- Expr -> TcM Schema
exprSchema Expr
expr
     case Schema -> Maybe Type
isMono Schema
s of
       Just Type
t  -> Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
       Maybe Type
Nothing -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Schema -> Error
ExpectedMono Schema
s)


-- | Check that the expression is well-formed, and compute its schema.
exprSchema :: Expr -> TcM Schema
exprSchema :: Expr -> TcM Schema
exprSchema Expr
expr =
  case Expr
expr of

    ELocated Range
rng Expr
t -> Range -> TcM Schema -> TcM Schema
forall a. Range -> TcM a -> TcM a
withRange Range
rng (Expr -> TcM Schema
exprSchema Expr
t)

    EList [Expr]
es Type
t ->
      do Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
         [Expr] -> (Expr -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Expr]
es ((Expr -> TcM ()) -> TcM ()) -> (Expr -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Expr
e ->
           do Type
t1 <- Expr -> TcM Type
exprType Expr
e
              String -> Type -> Type -> TcM ()
sameTypes String
"EList" Type
t1 Type
t

         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tSeq (Int -> Type
forall a. Integral a => a -> Type
tNum ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es)) Type
t

    ETuple [Expr]
es ->
      ([Type] -> Schema) -> TcM [Type] -> TcM Schema
forall a b. (a -> b) -> TcM a -> TcM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Schema
tMono (Type -> Schema) -> ([Type] -> Type) -> [Type] -> Schema
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
tTuple) ((Expr -> TcM Type) -> [Expr] -> TcM [Type]
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 Expr -> TcM Type
exprType [Expr]
es)

    ERec RecordMap Ident Expr
fs ->
      do RecordMap Ident Type
fs1 <- (Expr -> TcM Type)
-> RecordMap Ident Expr -> TcM (RecordMap Ident Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse Expr -> TcM Type
exprType RecordMap Ident Expr
fs
         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> Type
TRec RecordMap Ident Type
fs1

    ESet Type
_ Expr
e Selector
x Expr
v ->
       do Type
ty  <- Expr -> TcM Type
exprType Expr
e
          Type
expe <- Type -> Selector -> TcM Type
checkHas Type
ty Selector
x
          Type
has <- Expr -> TcM Type
exprType Expr
v
          String -> Type -> Type -> TcM ()
sameTypes String
"ESet" Type
expe Type
has
          Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
ty)

    ESel Expr
e Selector
sel -> do Type
ty <- Expr -> TcM Type
exprType Expr
e
                     Type
ty1 <- Type -> Selector -> TcM Type
checkHas Type
ty Selector
sel
                     Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
ty1)

    EIf Expr
e1 Expr
e2 Expr
e3 ->
      do Type
ty <- Expr -> TcM Type
exprType Expr
e1
         String -> Type -> Type -> TcM ()
sameTypes String
"EIf_condition" Type
tBit Type
ty

         Type
t1 <- Expr -> TcM Type
exprType Expr
e2
         Type
t2 <- Expr -> TcM Type
exprType Expr
e3
         String -> Type -> Type -> TcM ()
sameTypes String
"EIf_arms" Type
t1 Type
t2

         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono Type
t1

    ECase Expr
e Map Ident CaseAlt
as Maybe CaseAlt
d ->
      do Type
ty <- Expr -> TcM Type
exprType Expr
e
         case Type -> Type
tNoUser Type
ty of
           TNominal NominalType
nt [Type]
targs
             | Enum [EnumCon]
cons <- NominalType -> NominalTypeDef
ntDef NominalType
nt ->
              do Map Ident ([Type], Type)
alts <- (CaseAlt -> TcM ([Type], Type))
-> Map Ident CaseAlt -> TcM (Map Ident ([Type], Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Ident a -> f (Map Ident b)
traverse CaseAlt -> TcM ([Type], Type)
checkCaseAlt Map Ident CaseAlt
as
                 Maybe ([Type], Type)
dflt <- (CaseAlt -> TcM ([Type], Type))
-> Maybe CaseAlt -> TcM (Maybe ([Type], Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse CaseAlt -> TcM ([Type], Type)
checkCaseAlt Maybe CaseAlt
d
                 let resTypes :: [Type]
resTypes = (([Type], Type) -> Type) -> [([Type], Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ([Type], Type) -> Type
forall a b. (a, b) -> b
snd (Maybe ([Type], Type) -> [([Type], Type)]
forall a. Maybe a -> [a]
maybeToList Maybe ([Type], Type)
dflt [([Type], Type)] -> [([Type], Type)] -> [([Type], Type)]
forall a. [a] -> [a] -> [a]
++ Map Ident ([Type], Type) -> [([Type], Type)]
forall k a. Map k a -> [a]
Map.elems Map Ident ([Type], Type)
alts)
                 Type
resT <- case [Type]
resTypes of
                           []     -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Maybe Type -> Error
BadCase Maybe Type
forall a. Maybe a
Nothing)
                           Type
t : [Type]
ts ->
                             do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> Type -> Type -> TcM ()
sameTypes String
"ECase_alt_result" Type
t) [Type]
ts
                                Type -> TcM Type
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t

                 let su :: Subst
su = [Subst] -> Subst
mergeDistinctSubst
                            ((TParam -> Type -> Subst) -> [TParam] -> [Type] -> [Subst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TParam -> Type -> Subst
singleTParamSubst (NominalType -> [TParam]
ntParams NominalType
nt) [Type]
targs)
                     conMap :: Map Ident [Type]
conMap = [(Ident, [Type])] -> Map Ident [Type]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name -> Ident
nameIdent (EnumCon -> Name
ecName EnumCon
c)
                                           , Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnumCon -> [Type]
ecFields EnumCon
c)
                                           | EnumCon
c <- [EnumCon]
cons ]
                     checkCon :: (Ident, ([Type], b)) -> TcM ()
checkCon (Ident
c,([Type]
ts,b
_)) =
                       case Ident -> Map Ident [Type] -> Maybe [Type]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
c Map Ident [Type]
conMap of
                         Just [Type]
ts1 | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 ->
                                (Type -> Type -> TcM ()) -> [Type] -> [Type] -> TcM ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (String -> Type -> Type -> TcM ()
sameTypes String
"ECase_alt_field") [Type]
ts [Type]
ts1
                         Maybe [Type]
_ -> Error -> TcM ()
forall a. Error -> TcM a
reportError (Maybe Ident -> Error
BadCaseAlt (Ident -> Maybe Ident
forall a. a -> Maybe a
Just Ident
c))
                 ((Ident, ([Type], Type)) -> TcM ())
-> [(Ident, ([Type], Type))] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ident, ([Type], Type)) -> TcM ()
forall {b}. (Ident, ([Type], b)) -> TcM ()
checkCon (Map Ident ([Type], Type) -> [(Ident, ([Type], Type))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Ident ([Type], Type)
alts)
                 case Maybe ([Type], Type)
dflt of
                   Maybe ([Type], Type)
Nothing -> () -> TcM ()
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                   Just ([Type
t],Type
_) -> String -> Type -> Type -> TcM ()
sameTypes String
"ECase_default_arg" Type
t Type
ty
                   Maybe ([Type], Type)
_ -> Error -> TcM ()
forall a. Error -> TcM a
reportError (Maybe Ident -> Error
BadCaseAlt Maybe Ident
forall a. Maybe a
Nothing)
                 Schema -> TcM Schema
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Schema
tMono Type
resT)

           Type
_ -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Maybe Type -> Error
BadCase (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty))

    EComp Type
len Type
t Expr
e [[Match]]
mss ->
      do Kind -> Type -> TcM ()
checkTypeIs Kind
KNum Type
len
         Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t

         ([[(Name, Schema)]]
xs,[Type]
ls) <- [([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type]))
-> TcM [([(Name, Schema)], Type)]
-> TcM ([[(Name, Schema)]], [Type])
forall a b. (a -> b) -> TcM a -> TcM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([Match] -> TcM ([(Name, Schema)], Type))
-> [[Match]] -> TcM [([(Name, Schema)], Type)]
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 [Match] -> TcM ([(Name, Schema)], Type)
checkArm [[Match]]
mss
         -- XXX: check no duplicates
         Type
elT <- [(Name, Schema)] -> TcM Type -> TcM Type
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars ([[(Name, Schema)]] -> [(Name, Schema)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, Schema)]]
xs) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TcM Type
exprType Expr
e

         case [Type]
ls of
           [] -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           [Type]
_  -> Type -> Type -> TcM ()
convertible (Type -> Type -> Type
tSeq Type
len Type
t) (Type -> Type -> Type
tSeq ((Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMin [Type]
ls) Type
elT)

         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono (Type -> Type -> Type
tSeq Type
len Type
t))


    EVar Name
x -> Name -> TcM Schema
lookupVar Name
x

    ETAbs TParam
a Expr
e     ->
      do Forall [TParam]
as [Type]
p Type
t <- TParam -> TcM Schema -> TcM Schema
forall a. TParam -> TcM a -> TcM a
withTVar TParam
a (Expr -> TcM Schema
exprSchema Expr
e)
         Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((TParam -> Bool) -> [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TParam -> TParam -> Bool
forall a. Eq a => a -> a -> Bool
== TParam
a) [TParam]
as) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
           Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ TParam -> Error
RepeatedVariableInForall TParam
a

         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall (TParam
a TParam -> [TParam] -> [TParam]
forall a. a -> [a] -> [a]
: [TParam]
as) [Type]
p Type
t)

    ETApp Expr
e Type
t ->
      do Kind
k <- Type -> TcM Kind
checkType Type
t
         Schema
s <- Expr -> TcM Schema
exprSchema Expr
e
         case Schema
s of
           Forall (TParam
a : [TParam]
as) [Type]
ps Type
t1 ->
             do let vs :: Set TVar
vs = Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t

                [TVar] -> (TVar -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) ((TVar -> TcM ()) -> TcM ()) -> (TVar -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \TVar
b ->
                  Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TVar
b TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ TVar -> Error
Captured TVar
b

                let k' :: Kind
k' = TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
a
                Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k') (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k' Kind
k

                let su :: Subst
su = TParam -> Type -> Subst
singleTParamSubst TParam
a Type
t
                Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
ps) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t1)

           Forall [] [Type]
_ Type
_ -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadInstantiation

    EApp Expr
e1 Expr
e2 ->
      do Type
t1 <- Expr -> TcM Type
exprType Expr
e1
         Type
t2 <- Expr -> TcM Type
exprType Expr
e2

         case Type -> Type
tNoUser Type
t1 of
           TCon (TC TC
TCFun) [ Type
a, Type
b ]
              | SameIf [Type]
ps <- Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
a Type
t2 ->
                do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
                   Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
b)
           Type
tf -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Type -> Type -> Error
BadApplication Type
tf Type
t1)


    EAbs Name
x Type
t Expr
e    ->
      do Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
         Type
res <- Name -> Type -> TcM Type -> TcM Type
forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t (Expr -> TcM Type
exprType Expr
e)
         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tFun Type
t Type
res


    EProofAbs Type
p Expr
e ->
      do Kind -> Type -> TcM ()
checkTypeIs Kind
KProp Type
p
         Type -> TcM Schema -> TcM Schema
forall a. Type -> TcM a -> TcM a
withAsmp Type
p (TcM Schema -> TcM Schema) -> TcM Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ do Forall [TParam]
as [Type]
ps Type
t <- Expr -> TcM Schema
exprSchema Expr
e
                         Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Type
p Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps) Type
t

    EProofApp Expr
e ->
      do Forall [TParam]
as [Type]
ps Type
t <- Expr -> TcM Schema
exprSchema Expr
e
         case ([TParam]
as,[Type]
ps) of
           ([], Type
p:[Type]
qs) -> do Type -> TcM ()
proofObligation Type
p
                            Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall [] [Type]
qs Type
t)
           ([], [Type]
_)    -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadProofNoAbs
           ([TParam]
_,[Type]
_)      -> Error -> TcM Schema
forall a. Error -> TcM a
reportError ([TParam] -> Error
BadProofTyVars [TParam]
as)


    -- XXX: Check that defined things are distinct?
    EWhere Expr
e [DeclGroup]
dgs ->
      let go :: [DeclGroup] -> TcM Schema
go []       = Expr -> TcM Schema
exprSchema Expr
e
          go (DeclGroup
d : [DeclGroup]
ds) = do [(Name, Schema)]
xs <- DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
d
                           [(Name, Schema)] -> TcM Schema -> TcM Schema
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs ([DeclGroup] -> TcM Schema
go [DeclGroup]
ds)
      in [DeclGroup] -> TcM Schema
go [DeclGroup]
dgs


    EPropGuards [([Type], Expr)]
guards Type
typ ->
      do [([Type], Expr)] -> (([Type], Expr) -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([Type], Expr)]
guards ((([Type], Expr) -> TcM ()) -> TcM ())
-> (([Type], Expr) -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \([Type]
prop, Expr
e) ->
           do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Kind -> Type -> TcM ()
checkTypeIs Kind
KProp) [Type]
prop
              Type
eTyp <- Expr -> TcM Type
exprType Expr
e
              String -> Type -> Type -> TcM ()
sameTypes String
"EPropGuards" Type
typ Type
eTyp
         Schema -> TcM Schema
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Schema
tMono Type
typ)


checkCaseAlt :: CaseAlt -> TcM ([Type], Type)
checkCaseAlt :: CaseAlt -> TcM ([Type], Type)
checkCaseAlt (CaseAlt [(Name, Type)]
xs Expr
e) =
  do Type
ty <- ((Name, Type) -> TcM Type -> TcM Type)
-> TcM Type -> [(Name, Type)] -> TcM Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Type) -> TcM Type -> TcM Type
forall {a}. (Name, Type) -> TcM a -> TcM a
addVar (Expr -> TcM Type
exprType Expr
e) [(Name, Type)]
xs
     ([Type], Type) -> TcM ([Type], Type)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd [(Name, Type)]
xs, Type
ty)
  where
  addVar :: (Name, Type) -> TcM a -> TcM a
addVar (Name
x,Type
t) = Name -> Type -> TcM a -> TcM a
forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t

checkHas :: Type -> Selector -> TcM Type
checkHas :: Type -> Selector -> TcM Type
checkHas Type
t Selector
sel =
  case Selector
sel of

    TupleSel Int
n Maybe Int
mb ->

      case Type -> Type
tNoUser Type
t of
        TCon (TC (TCTuple Int
sz)) [Type]
ts ->
          do case Maybe Int
mb of
               Just Int
sz1 ->
                 Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
sz1) (Error -> TcM ()
forall a. Error -> TcM a
reportError (Int -> Int -> Error
UnexpectedTupleShape Int
sz1 Int
sz))
               Maybe Int
Nothing  -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
             Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Int -> Int -> Error
TupleSelectorOutOfRange Int
n Int
sz)
             Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcM Type) -> Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ [Type]
ts [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
n

        TCon (TC TC
TCSeq) [Type
s,Type
elT] ->
           do Type
res <- Type -> Selector -> TcM Type
checkHas Type
elT Selector
sel
              Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
s,Type
res])

        TCon (TC TC
TCFun) [Type
a,Type
b] ->
            do Type
res <- Type -> Selector -> TcM Type
checkHas Type
b Selector
sel
               Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])

        Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t


    RecordSel Ident
f Maybe [Ident]
mb ->
      case Type -> Type
tNoUser Type
t of
        TRec RecordMap Ident Type
fs ->

          do case Maybe [Ident]
mb of
               Maybe [Ident]
Nothing -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just [Ident]
fs1 ->
                 do let ns :: [Ident]
ns  = Set Ident -> [Ident]
forall a. Set a -> [a]
Set.toList (RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs)
                        ns1 :: [Ident]
ns1 = [Ident] -> [Ident]
forall a. Ord a => [a] -> [a]
sort [Ident]
fs1
                    Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ident]
ns [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== [Ident]
ns1) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                      Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> [Ident] -> Error
UnexpectedRecordShape [Ident]
ns1 [Ident]
ns

             case Ident -> RecordMap Ident Type -> Maybe Type
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f RecordMap Ident Type
fs of
               Maybe Type
Nothing -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Ident -> [Ident] -> Error
MissingField Ident
f ([Ident] -> Error) -> [Ident] -> Error
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident Type
fs
               Just Type
ft -> Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ft

        TCon (TC TC
TCSeq) [Type
s,Type
elT] -> do Type
res <- Type -> Selector -> TcM Type
checkHas Type
elT Selector
sel
                                      Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
s,Type
res])

        TCon (TC TC
TCFun) [Type
a,Type
b]   -> do Type
res <- Type -> Selector -> TcM Type
checkHas Type
b Selector
sel
                                      Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])


        Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t


    -- XXX: Remove this?
    ListSel Int
_ Maybe Int
mb ->
      case Type -> Type
tNoUser Type
t of
        TCon (TC TC
TCSeq) [ Type
n, Type
elT ] ->

          do case Maybe Int
mb of
               Maybe Int
Nothing  -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just Int
len ->
                 case Type -> Type
tNoUser Type
n of
                   TCon (TC (TCNum Integer
m)) []
                     | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                   Type
_ -> Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Error
UnexpectedSequenceShape Int
len Type
n

             Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
elT

        Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t




-- | Check if the one type is convertible to the other.
convertible :: Type -> Type -> TcM ()
convertible :: Type -> Type -> TcM ()
convertible Type
t1 Type
t2
  | Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
k2    = Error -> TcM ()
forall a. Error -> TcM a
reportError (Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k2)
  | Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum  = Type -> TcM ()
proofObligation (Type
t1 Type -> Type -> Type
=#= Type
t2)
  where
  k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
  k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2

convertible Type
t1 Type
t2 = Type -> Type -> TcM ()
go Type
t1 Type
t2
  where
  go :: Type -> Type -> TcM ()
go Type
ty1 Type
ty2 =
    let err :: TcM a
err   = Error -> TcM a
forall a. Error -> TcM a
reportError (Error -> TcM a) -> Error -> TcM a
forall a b. (a -> b) -> a -> b
$ String -> Schema -> Schema -> Error
TypeMismatch String
"convertible" (Type -> Schema
tMono Type
ty1) (Type -> Schema
tMono Type
ty2)
        other :: Type
other = Type -> Type
tNoUser Type
ty2

        goMany :: [Type] -> [Type] -> TcM ()
goMany [] []             = () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        goMany (Type
x : [Type]
xs) (Type
y : [Type]
ys) = Type -> Type -> TcM ()
convertible Type
x Type
y TcM () -> TcM () -> TcM ()
forall a b. TcM a -> TcM b -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Type] -> [Type] -> TcM ()
goMany [Type]
xs [Type]
ys
        goMany [Type]
_ [Type]
_               = TcM ()
forall {a}. TcM a
err

    in case Type
ty1 of
         TUser Name
_ [Type]
_ Type
s   -> Type -> Type -> TcM ()
go Type
s Type
ty2

         TVar TVar
x        -> case Type
other of
                            TVar TVar
y | TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y  -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                            Type
_                -> TcM ()
forall {a}. TcM a
err

         TCon TCon
tc1 [Type]
ts1  -> case Type
other of
                            TCon TCon
tc2 [Type]
ts2
                               | TCon
tc1 TCon -> TCon -> Bool
forall a. Eq a => a -> a -> Bool
== TCon
tc2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
                            Type
_ -> TcM ()
forall {a}. TcM a
err

         TNominal NominalType
nt1 [Type]
ts1 ->
            case Type
other of
              TNominal NominalType
nt2 [Type]
ts2
                | NominalType
nt1 NominalType -> NominalType -> Bool
forall a. Eq a => a -> a -> Bool
== NominalType
nt2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
              Type
_ -> TcM ()
forall {a}. TcM a
err

         TRec RecordMap Ident Type
fs ->
           case Type
other of
             TRec RecordMap Ident Type
gs ->
               do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
gs) TcM ()
forall {a}. TcM a
err
                  [Type] -> [Type] -> TcM ()
goMany (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs) (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
gs)
             Type
_ -> TcM ()
forall {a}. TcM a
err


--------------------------------------------------------------------------------

-- | Check a declaration. The boolean indicates if we should check the siganture
checkDecl :: Bool -> Decl -> TcM (Name, Schema)
checkDecl :: Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
checkSig Decl
d =
  case Decl -> DeclDef
dDefinition Decl
d of

    DeclDef
DPrim ->
      do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
         (Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)

    DForeign FFIFunType
_ Maybe Expr
me ->
      do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
         (Expr -> TcM ()) -> Maybe Expr -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Expr -> TcM ()
checkExpr Maybe Expr
me
         (Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)

    DExpr Expr
e ->
      do let s :: Schema
s = Decl -> Schema
dSignature Decl
d
         Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema Schema
s
         Expr -> TcM ()
checkExpr Expr
e
         (Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Schema
s)

  where
  checkExpr :: Expr -> TcM ()
checkExpr Expr
e =
    do let s :: Schema
s = Decl -> Schema
dSignature Decl
d
       Schema
s1 <- Expr -> TcM Schema
exprSchema Expr
e
       let nm :: Name
nm = Decl -> Name
dName Decl
d
           loc :: String
loc = String
"definition of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
nm) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                          String
", at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Range -> Doc
forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
nm))
       String -> Schema -> Schema -> TcM ()
sameSchemas String
loc Schema
s Schema
s1

checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
dg =
  case DeclGroup
dg of
    NonRecursive Decl
d -> do (Name, Schema)
x <- Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
True Decl
d
                         [(Name, Schema)] -> TcM [(Name, Schema)]
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Schema)
x]
    Recursive [Decl]
ds ->
      do [(Name, Schema)]
xs <- [Decl] -> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
ds ((Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)])
-> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
forall a b. (a -> b) -> a -> b
$ \Decl
d ->
                  do Schema -> TcM ()
checkSchema (Decl -> Schema
dSignature Decl
d)
                     (Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
         [(Name, Schema)] -> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs (TcM [(Name, Schema)] -> TcM [(Name, Schema)])
-> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
forall a b. (a -> b) -> a -> b
$ (Decl -> TcM (Name, Schema)) -> [Decl] -> TcM [(Name, Schema)]
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 (Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
False) [Decl]
ds


checkMatch :: Match -> TcM ((Name, Schema), Type)
checkMatch :: Match -> TcM ((Name, Schema), Type)
checkMatch Match
ma =
  case Match
ma of
    From Name
x Type
len Type
elt Expr
e ->
      do Kind -> Type -> TcM ()
checkTypeIs Kind
KNum Type
len
         Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
elt
         Type
t1 <- Expr -> TcM Type
exprType Expr
e
         case Type -> Type
tNoUser Type
t1 of
           TCon (TC TC
TCSeq) [ Type
l, Type
el ]
             | SameIf [Type]
ps <- Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
elt Type
el ->
               do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
                  ((Name, Schema), Type) -> TcM ((Name, Schema), Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
x, Type -> Schema
tMono Type
elt), Type
l)
             | Bool
otherwise -> Error -> TcM ((Name, Schema), Type)
forall a. Error -> TcM a
reportError (Error -> TcM ((Name, Schema), Type))
-> Error -> TcM ((Name, Schema), Type)
forall a b. (a -> b) -> a -> b
$ String -> Schema -> Schema -> Error
TypeMismatch String
"From" (Type -> Schema
tMono Type
elt) (Type -> Schema
tMono Type
el)


           Type
_ -> Error -> TcM ((Name, Schema), Type)
forall a. Error -> TcM a
reportError (Error -> TcM ((Name, Schema), Type))
-> Error -> TcM ((Name, Schema), Type)
forall a b. (a -> b) -> a -> b
$ Type -> Error
BadMatch Type
t1

    Let Decl
d -> do (Name, Schema)
x <- Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
True Decl
d
                ((Name, Schema), Type) -> TcM ((Name, Schema), Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, Schema)
x, Int -> Type
forall a. Integral a => a -> Type
tNum (Int
1 :: Int))

checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm []   = Error -> TcM ([(Name, Schema)], Type)
forall a. Error -> TcM a
reportError Error
EmptyArm
checkArm [Match
m]  = do ((Name, Schema)
x,Type
l) <- Match -> TcM ((Name, Schema), Type)
checkMatch Match
m
                   ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Schema)
x], Type
l)
checkArm (Match
m : [Match]
ms) =
  do ((Name, Schema)
x, Type
l)   <- Match -> TcM ((Name, Schema), Type)
checkMatch Match
m
     ([(Name, Schema)]
xs, Type
l1) <- [(Name, Schema)]
-> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)
x] (TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
-> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a b. (a -> b) -> a -> b
$ [Match] -> TcM ([(Name, Schema)], Type)
checkArm [Match]
ms
     let newLen :: Type
newLen = Type -> Type -> Type
tMul Type
l Type
l1
     ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
-> ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a b. (a -> b) -> a -> b
$ if (Name, Schema) -> Name
forall a b. (a, b) -> a
fst (Name, Schema)
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, Schema) -> Name) -> [(Name, Schema)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Schema) -> Name
forall a b. (a, b) -> a
fst [(Name, Schema)]
xs
                 then ([(Name, Schema)]
xs, Type
newLen)
                 else ((Name, Schema)
x (Name, Schema) -> [(Name, Schema)] -> [(Name, Schema)]
forall a. a -> [a] -> [a]
: [(Name, Schema)]
xs, Type
newLen)




--------------------------------------------------------------------------------

data RO = RO
  { RO -> Map Int TParam
roTVars   :: Map Int TParam
  , RO -> [Type]
roAsmps   :: [Prop]
  , RO -> Range
roRange   :: Range
  , RO -> Map Name Schema
roVars    :: Map Name Schema
  }

type ProofObligation = Schema -- but the type is of kind Prop

data RW = RW
  { RW -> [Schema]
woProofObligations :: [ProofObligation]
  }

newtype TcM a = TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a)

instance Functor TcM where
  fmap :: forall a b. (a -> b) -> TcM a -> TcM b
fmap = (a -> b) -> TcM a -> TcM b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance A.Applicative TcM where
  pure :: forall a. a -> TcM a
pure a
a = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
  <*> :: forall a b. TcM (a -> b) -> TcM a -> TcM b
(<*>) = TcM (a -> b) -> TcM a -> TcM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad TcM where
  return :: forall a. a -> TcM a
return      = a -> TcM a
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m >>= :: forall a b. TcM a -> (a -> TcM b) -> TcM b
>>= a -> TcM b
f = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b -> TcM b
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (do a
a <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
                        let TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
m1 = a -> TcM b
f a
a
                        ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
m1)

runTcM :: InferInput -> TcM a -> Either (Range, Error) (a, [ProofObligation])
runTcM :: forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) =
  case ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> RO -> RW -> (Either (Range, Error) a, RW)
forall (m :: * -> *) a r. RunM m a r => m a -> r
runM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m RO
ro RW
rw of
    (Left (Range, Error)
err, RW
_) -> (Range, Error) -> Either (Range, Error) (a, [Schema])
forall a b. a -> Either a b
Left (Range, Error)
err
    (Right a
a, RW
s)  -> (a, [Schema]) -> Either (Range, Error) (a, [Schema])
forall a b. b -> Either a b
Right (a
a, RW -> [Schema]
woProofObligations RW
s)
  where
  allPs :: ModParamNames
allPs = InferInput -> ModParamNames
inpParams InferInput
env

  ro :: RO
ro = RO { roTVars :: Map Int TParam
roTVars = [(Int, TParam)] -> Map Int TParam
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TParam -> Int
tpUnique TParam
x, TParam
x)
                                      | ModTParam
tp <- Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
allPs)
                                      , let x :: TParam
x = ModTParam -> TParam
mtpParam ModTParam
tp ]
          , roAsmps :: [Type]
roAsmps = (Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
allPs)
          , roRange :: Range
roRange = Range
emptyRange
          , roVars :: Map Name Schema
roVars  = [Map Name Schema] -> Map Name Schema
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
                        [ (ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
allPs)
                        , InferInput -> Map Name Schema
inpVars InferInput
env
                        , [(Name, Schema)] -> Map Name Schema
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                            [ (Name, Schema)
c
                            | NominalType
nt <- Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (InferInput -> Map Name NominalType
inpNominalTypes InferInput
env)
                            , (Name, Schema)
c  <- NominalType -> [(Name, Schema)]
nominalTypeConTypes NominalType
nt
                            ]
                        ]

          }
  rw :: RW
rw = RW { woProofObligations :: [Schema]
woProofObligations = [] }


data Error =
    TypeMismatch String Schema Schema    -- ^ expected, actual
  | ExpectedMono Schema           -- ^ expected a mono type, got this
  | TupleSelectorOutOfRange Int Int
  | MissingField Ident [Ident]
  | UnexpectedTupleShape Int Int
  | UnexpectedRecordShape [Ident] [Ident]
  | UnexpectedSequenceShape Int Type
  | BadSelector Selector Type
  | BadInstantiation
  | Captured TVar
  | BadProofNoAbs
  | BadProofTyVars [TParam]
  | KindMismatch Kind Kind
  | NotEnoughArgumentsInKind Kind
  | BadApplication Type Type
  | FreeTypeVariable TVar
  | BadTypeApplication Kind [Kind]
  | RepeatedVariableInForall TParam
  | BadMatch Type
  | EmptyArm
  | UndefinedTypeVaraible TVar
  | UndefinedVariable Name
  | BadCase (Maybe Type)
  | BadCaseAlt (Maybe Ident)
    deriving Int -> Error -> String -> String
[Error] -> String -> String
Error -> String
(Int -> Error -> String -> String)
-> (Error -> String) -> ([Error] -> String -> String) -> Show Error
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Error -> String -> String
showsPrec :: Int -> Error -> String -> String
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> String -> String
showList :: [Error] -> String -> String
Show

reportError :: Error -> TcM a
reportError :: forall a. Error -> TcM a
reportError Error
e = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     (Range, Error)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
(Range, Error)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise (RO -> Range
roRange RO
ro, Error
e)

withTVar :: TParam -> TcM a -> TcM a
withTVar :: forall a. TParam -> TcM a -> TcM a
withTVar TParam
a (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roTVars = Map.insert (tpUnique a) a (roTVars ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m

withRange :: Range -> TcM a -> TcM a
withRange :: forall a. Range -> TcM a -> TcM a
withRange Range
rng (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roRange = rng } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m

withAsmp :: Prop -> TcM a -> TcM a
withAsmp :: forall a. Type -> TcM a -> TcM a
withAsmp Type
p (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roAsmps = p : roAsmps ro } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m

withVar :: Name -> Type -> TcM a -> TcM a
withVar :: forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t = [(Name, Schema)] -> TcM a -> TcM a
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name
x,Type -> Schema
tMono Type
t)]

withVars :: [(Name, Schema)] -> TcM a -> TcM a
withVars :: forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roVars = Map.union (Map.fromList xs) (roVars ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m

proofObligation :: Prop -> TcM ()
proofObligation :: Type -> TcM ()
proofObligation Type
p = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) () -> TcM ()
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
 -> TcM ())
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
-> TcM ()
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     (RW -> RW)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ ((RW -> RW)
 -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ())
-> (RW -> RW)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { woProofObligations =
                             Forall (Map.elems (roTVars ro)) (roAsmps ro) p
                           : woProofObligations rw }

lookupTVar :: TVar -> TcM Kind
lookupTVar :: TVar -> TcM Kind
lookupTVar TVar
x =
  case TVar
x of
    TVFree {} -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (TVar -> Error
FreeTypeVariable TVar
x)
    TVBound TParam
tpv ->
       do let u :: Int
u = TParam -> Int
tpUnique TParam
tpv
              k :: Kind
k = TParam -> Kind
tpKind TParam
tpv
          RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
          case Int -> Map Int TParam -> Maybe TParam
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
u (RO -> Map Int TParam
roTVars RO
ro) of
            Just TParam
tp
              | TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
tp Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k  -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
              | Bool
otherwise       -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch (TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
tp) Kind
k
            Maybe TParam
Nothing  -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ TVar -> Error
UndefinedTypeVaraible TVar
x

lookupVar :: Name -> TcM Schema
lookupVar :: Name -> TcM Schema
lookupVar Name
x =
  do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     case Name -> Map Name Schema -> Maybe Schema
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (RO -> Map Name Schema
roVars RO
ro) of
       Just Schema
s -> Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Schema
s
       Maybe Schema
Nothing -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Error -> TcM Schema) -> Error -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Name -> Error
UndefinedVariable Name
x


instance PP Error where
  ppPrec :: Int -> Error -> Doc
ppPrec Int
_ Error
err =
    case Error
err of

      TypeMismatch String
what Schema
expected Schema
actual ->
        Doc -> [Doc] -> Doc
ppErr (Doc
"Type mismatch in" Doc -> Doc -> Doc
<+> String -> Doc
text String
what)
          [ Doc
"Expected:" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
expected
          , Doc
"Actual  :" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
actual
          ]

      ExpectedMono Schema
s ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Not a monomorphic type"
          [ Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
s ]

      TupleSelectorOutOfRange Int
sel Int
sz ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Tuple selector out of range"
          [ Doc
"Selector:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
sel
          , Doc
"Size    :" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
sz
          ]

      MissingField Ident
f [Ident]
fs ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Invalid record selector"
          [ Doc
"Field: " Doc -> Doc -> Doc
<+> Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f
          , Doc
"Fields:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
fs)
          ]

      UnexpectedTupleShape Int
expected Int
actual ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected tuple shape"
          [ Doc
"Expected:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
expected
          , Doc
"Actual  :" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
actual
          ]

      UnexpectedRecordShape [Ident]
expected [Ident]
actual ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected record shape"
          [ Doc
"Expected:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
expected)
          , Doc
"Actual  :" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
actual)
          ]

      UnexpectedSequenceShape Int
n Type
t ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected sequence shape"
          [ Doc
"Expected:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
n
          , Doc
"Actual  :" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
          ]

      BadSelector Selector
sel Type
t ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Bad selector"
          [ Doc
"Selector:" Doc -> Doc -> Doc
<+> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel
          , Doc
"Type    :" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
          ]

      Error
BadInstantiation ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Bad instantiation" []

      Captured TVar
x ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Captured type variable"
          [ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]

      Error
BadProofNoAbs ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Proof application without a proof abstraction" []

      BadProofTyVars [TParam]
xs ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Proof application with type abstraction"
          [ Doc
"Type parameter:" Doc -> Doc -> Doc
<+> TParam -> Doc
forall a. PP a => a -> Doc
pp TParam
x | TParam
x <- [TParam]
xs ]

      KindMismatch Kind
expected Kind
actual ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Kind mismatch"
          [ Doc
"Expected:" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
expected
          , Doc
"Actual  :" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
actual
          ]

      NotEnoughArgumentsInKind Kind
k ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Not enough arguments in kind" [ Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
k ]

      BadApplication Type
t1 Type
t2 ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Bad application"
          [ Doc
"Function:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t1
          , Doc
"Argument:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t2
          ]

      FreeTypeVariable TVar
x ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Free type variable"
          [ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]

      BadTypeApplication Kind
kf [Kind]
ka ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Bad type application"
          [ Doc
"Function :" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
kf
          , Doc
"Arguments:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Kind -> Doc) -> [Kind] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> Doc
forall a. PP a => a -> Doc
pp [Kind]
ka)
          ]

      RepeatedVariableInForall TParam
x ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Repeated variable in forall"
          [ Doc
"Variable:" Doc -> Doc -> Doc
<+> TParam -> Doc
forall a. PP a => a -> Doc
pp TParam
x ]

      BadMatch Type
t ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Bad match"
          [ Doc
"Type:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t ]

      Error
EmptyArm -> Doc -> [Doc] -> Doc
ppErr Doc
"Empty comprehension arm" []

      UndefinedTypeVaraible TVar
x ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Undefined type variable"
          [ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]

      UndefinedVariable Name
x ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Undefined variable"
          [ Doc
"Variable:" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x ]

      BadCase Maybe Type
mbt ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Malformed cased expression" ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        case Maybe Type
mbt of
          Just Type
t  -> [ Doc
"Expected: `enum` type", Doc
"Actual:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t ]
          Maybe Type
Nothing -> [ Doc
"Empty alternatives" ]

      BadCaseAlt Maybe Ident
mbCon ->
        Doc -> [Doc] -> Doc
ppErr Doc
"Malformed case alternative" ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        [ case Maybe Ident
mbCon of
            Just Ident
c  -> Doc
"Alternative for constructor" Doc -> Doc -> Doc
<+> Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
c
            Maybe Ident
Nothing -> Doc
"Default alternative"
        ]

    where
    ppErr :: Doc -> [Doc] -> Doc
ppErr Doc
x [Doc]
ys = Doc -> Int -> Doc -> Doc
hang Doc
x Int
2 ([Doc] -> Doc
vcat [ Doc
"•" Doc -> Doc -> Doc
<+> Doc
y | Doc
y <- [Doc]
ys ])