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


import Cryptol.Parser.Position(thing)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap

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


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

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

tcModule :: InferInput -> Module -> Either Error [ ProofObligation ]
tcModule :: InferInput -> Module -> Either Error [Schema]
tcModule InferInput
env Module
m = case InferInput -> TcM () -> Either Error ((), [Schema])
forall a. InferInput -> TcM a -> Either Error (a, [Schema])
runTcM InferInput
env TcM ()
check of
                   Left Error
err -> Error -> Either Error [Schema]
forall a b. a -> Either a b
Left Error
err
                   Right (()
_,[Schema]
ps) -> [Schema] -> Either Error [Schema]
forall a b. b -> Either a b
Right [Schema]
ps
  where check :: TcM ()
check = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
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
mParamTypes Module
m)))
        k1 :: TcM ()
k1    = (Prop -> TcM () -> TcM ()) -> TcM () -> [Prop] -> TcM ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> TcM () -> TcM ()
forall a. Prop -> TcM a -> TcM a
withAsmp TcM ()
k2 ((Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing (Module -> [Located Prop]
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (Module -> Map Name ModVParam
mParamFuns Module
m)))
              (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> TcM ()
checkDecls (Module -> [DeclGroup]
mDecls Module
m)


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

checkDecls :: [DeclGroup] -> TcM ()
checkDecls :: [DeclGroup] -> TcM ()
checkDecls [DeclGroup]
decls =
  case [DeclGroup]
decls of
    [] -> () -> TcM ()
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 :: Prop -> TcM Kind
checkType Prop
ty =
  case Prop
ty of
    TUser Name
_ [Prop]
_ Prop
t -> Prop -> TcM Kind
checkType Prop
t    -- Maybe check synonym too?

    TCon TCon
tc [Prop]
ts ->
      do [Kind]
ks <- (Prop -> TcM Kind) -> [Prop] -> TcM [Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Prop -> TcM Kind
checkType [Prop]
ts
         Kind -> [Kind] -> TcM Kind
checkKind (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
tc) [Kind]
ks

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

    TRec RecordMap Ident Prop
fs ->
      do RecordMap Ident Prop -> (Prop -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RecordMap Ident Prop
fs ((Prop -> TcM ()) -> TcM ()) -> (Prop -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Prop
t ->
           do Kind
k <- Prop -> TcM Kind
checkType Prop
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     Kind
KNum     -> Kind -> TcM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     Kind
KType    -> Kind -> TcM Kind
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 -> Prop -> TcM ()
checkTypeIs Kind
k Prop
ty =
  do Kind
k1 <- Prop -> TcM Kind
checkType Prop
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 [Prop]
ps Prop
t) = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
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 (Prop -> TcM ()) -> [Prop] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Kind -> Prop -> TcM ()
checkTypeIs Kind
KProp) [Prop]
ps
                   Kind -> Prop -> TcM ()
checkTypeIs Kind
KType Prop
t


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

instance Same a => Same [a] where
  same :: [a] -> [a] -> Bool
same [] [] = Bool
True
  same (a
x : [a]
xs) (a
y : [a]
ys) = a -> a -> Bool
forall a. Same a => a -> a -> Bool
same a
x a
y Bool -> Bool -> Bool
&& [a] -> [a] -> Bool
forall a. Same a => a -> a -> Bool
same [a]
xs [a]
ys
  same [a]
_ [a]
_ = Bool
False

instance Same Type where
  same :: Prop -> Prop -> Bool
same Prop
t1 Prop
t2 = Prop -> Prop
tNoUser Prop
t1 Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop -> Prop
tNoUser Prop
t2

instance Same Schema where
  same :: Schema -> Schema -> Bool
same (Forall [TParam]
xs [Prop]
ps Prop
s) (Forall [TParam]
ys [Prop]
qs Prop
t) = [TParam] -> [TParam] -> Bool
forall a. Same a => a -> a -> Bool
same [TParam]
xs [TParam]
ys Bool -> Bool -> Bool
&& [Prop] -> [Prop] -> Bool
forall a. Same a => a -> a -> Bool
same [Prop]
ps [Prop]
qs Bool -> Bool -> Bool
&& Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
s Prop
t

instance Same TParam where
  same :: TParam -> TParam -> Bool
same TParam
x TParam
y = 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 Prop
exprType Expr
expr =
  do Schema
s <- Expr -> TcM Schema
exprSchema Expr
expr
     case Schema -> Maybe Prop
isMono Schema
s of
       Just Prop
t  -> Prop -> TcM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t
       Maybe Prop
Nothing -> Error -> TcM Prop
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

    EList [Expr]
es Prop
t ->
      do Kind -> Prop -> TcM ()
checkTypeIs Kind
KType Prop
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 Prop
t1 <- Expr -> TcM Prop
exprType Expr
e
              Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
t1 Prop
t) (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
$ String -> Schema -> Schema -> Error
TypeMismatch String
"EList" (Prop -> Schema
tMono Prop
t) (Prop -> Schema
tMono Prop
t1)

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

    ETuple [Expr]
es ->
      ([Prop] -> Schema) -> TcM [Prop] -> TcM Schema
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Prop -> Schema
tMono (Prop -> Schema) -> ([Prop] -> Prop) -> [Prop] -> Schema
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> Prop
tTuple) ((Expr -> TcM Prop) -> [Expr] -> TcM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> TcM Prop
exprType [Expr]
es)

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

    ESet Prop
_ Expr
e Selector
x Expr
v ->
       do Prop
ty  <- Expr -> TcM Prop
exprType Expr
e
          Prop
expe <- Prop -> Selector -> TcM Prop
checkHas Prop
ty Selector
x
          Prop
has <- Expr -> TcM Prop
exprType Expr
v
          Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
expe Prop
has) (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
$
               String -> Schema -> Schema -> Error
TypeMismatch String
"ESet" (Prop -> Schema
tMono Prop
expe) (Prop -> Schema
tMono Prop
has)
          Schema -> TcM Schema
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Schema
tMono Prop
ty)

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

    EIf Expr
e1 Expr
e2 Expr
e3 ->
      do Prop
ty <- Expr -> TcM Prop
exprType Expr
e1
         Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
tBit Prop
ty) (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
$ String -> Schema -> Schema -> Error
TypeMismatch String
"EIf_condition" (Prop -> Schema
tMono Prop
tBit) (Prop -> Schema
tMono Prop
ty)

         Prop
t1 <- Expr -> TcM Prop
exprType Expr
e2
         Prop
t2 <- Expr -> TcM Prop
exprType Expr
e3
         Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
t1 Prop
t2) (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
$ String -> Schema -> Schema -> Error
TypeMismatch String
"EIf_arms" (Prop -> Schema
tMono Prop
t1) (Prop -> Schema
tMono Prop
t2)

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

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

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

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

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


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

    ETAbs TParam
a Expr
e     ->
      do Forall [TParam]
as [Prop]
p Prop
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 (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Prop] -> Prop -> Schema
Forall (TParam
a TParam -> [TParam] -> [TParam]
forall a. a -> [a] -> [a]
: [TParam]
as) [Prop]
p Prop
t)

    ETApp Expr
e Prop
t ->
      do Kind
k <- Prop -> TcM Kind
checkType Prop
t
         Schema
s <- Expr -> TcM Schema
exprSchema Expr
e
         case Schema
s of
           Forall (TParam
a : [TParam]
as) [Prop]
ps Prop
t1 ->
             do let vs :: Set TVar
vs = Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
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 -> Prop -> Subst
singleTParamSubst TParam
a Prop
t
                Schema -> TcM Schema
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Prop]
ps) (Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t1)

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

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

         case Prop -> Prop
tNoUser Prop
t1 of
           TCon (TC TC
TCFun) [ Prop
a, Prop
b ]
              | Prop -> Prop -> Bool
forall a. Same a => a -> a -> Bool
same Prop
a Prop
t2 -> Schema -> TcM Schema
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Schema
tMono Prop
b)
           Prop
tf -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Prop -> Prop -> Error
BadApplication Prop
tf Prop
t1)


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


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

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


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

    TupleSel Int
n Maybe Int
mb ->

      case Prop -> Prop
tNoUser Prop
t of
        TCon (TC (TCTuple Int
sz)) [Prop]
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 (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)
             Prop -> TcM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> TcM Prop) -> Prop -> TcM Prop
forall a b. (a -> b) -> a -> b
$ [Prop]
ts [Prop] -> Int -> Prop
forall a. [a] -> Int -> a
!! Int
n

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

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

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


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

          do case Maybe [Ident]
mb of
               Maybe [Ident]
Nothing -> () -> TcM ()
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 Prop -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Prop
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 Prop -> Maybe Prop
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f RecordMap Ident Prop
fs of
               Maybe Prop
Nothing -> Error -> TcM Prop
forall a. Error -> TcM a
reportError (Error -> TcM Prop) -> Error -> TcM Prop
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 Prop -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident Prop
fs
               Just Prop
ft -> Prop -> TcM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
ft

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

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


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


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

          do case Maybe Int
mb of
               Maybe Int
Nothing  -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just Int
len ->
                 case Prop -> Prop
tNoUser Prop
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 (m :: * -> *) a. Monad m => a -> m a
return ()
                   Prop
_ -> Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Int -> Prop -> Error
UnexpectedSequenceShape Int
len Prop
n

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

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




-- | Check if the one type is convertible to the other.
convertible :: Type -> Type -> TcM ()
convertible :: Prop -> Prop -> TcM ()
convertible Prop
t1 Prop
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  = Prop -> TcM ()
proofObligation (Prop
t1 Prop -> Prop -> Prop
=#= Prop
t2)
  where
  k1 :: Kind
k1 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t1
  k2 :: Kind
k2 = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t2

convertible Prop
t1 Prop
t2 = Prop -> Prop -> TcM ()
go Prop
t1 Prop
t2
  where
  go :: Prop -> Prop -> TcM ()
go Prop
ty1 Prop
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" (Prop -> Schema
tMono Prop
ty1) (Prop -> Schema
tMono Prop
ty2)
        other :: Prop
other = Prop -> Prop
tNoUser Prop
ty2

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

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

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

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

         TRec RecordMap Ident Prop
fs ->
           case Prop
other of
             TRec RecordMap Ident Prop
gs ->
               do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RecordMap Ident Prop -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Prop
fs Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Prop -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Prop
gs) TcM ()
forall a. TcM a
err
                  [Prop] -> [Prop] -> TcM ()
goMany (RecordMap Ident Prop -> [Prop]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Prop
fs) (RecordMap Ident Prop -> [Prop]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Prop
gs)
             Prop
_ -> 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 (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
         Schema
s1 <- Expr -> TcM Schema
exprSchema Expr
e
         Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Schema -> Schema -> Bool
forall a. Same a => a -> a -> Bool
same Schema
s Schema
s1) (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
$ String -> Schema -> Schema -> Error
TypeMismatch String
"DExpr" Schema
s Schema
s1
         (Name, Schema) -> TcM (Name, Schema)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Schema
s)

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 (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 (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)
mapM (Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
False) [Decl]
ds


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


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

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

checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm :: [Match] -> TcM ([(Name, Schema)], Prop)
checkArm []   = Error -> TcM ([(Name, Schema)], Prop)
forall a. Error -> TcM a
reportError Error
EmptyArm
checkArm [Match
m]  = do ((Name, Schema)
x,Prop
l) <- Match -> TcM ((Name, Schema), Prop)
checkMatch Match
m
                   ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Schema)
x], Prop
l)
checkArm (Match
m : [Match]
ms) =
  do ((Name, Schema)
x, Prop
l)   <- Match -> TcM ((Name, Schema), Prop)
checkMatch Match
m
     ([(Name, Schema)]
xs, Prop
l1) <- [(Name, Schema)]
-> TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)
x] (TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop))
-> TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
forall a b. (a -> b) -> a -> b
$ [Match] -> TcM ([(Name, Schema)], Prop)
checkArm [Match]
ms
     let newLen :: Prop
newLen = Prop -> Prop -> Prop
tMul Prop
l Prop
l1
     ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop))
-> ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
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 (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, Prop
newLen)
                 else ((Name, Schema)
x (Name, Schema) -> [(Name, Schema)] -> [(Name, Schema)]
forall a. a -> [a] -> [a]
: [(Name, Schema)]
xs, Prop
newLen)




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

data RO = RO
  { RO -> Map Int TParam
roTVars   :: Map Int TParam
  , RO -> [Prop]
roAsmps   :: [Prop]
  , 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 Error (StateT RW Id)) a)

instance Functor TcM where
  fmap :: (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 :: a -> TcM a
pure  = a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: 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 :: a -> TcM a
return a
a    = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM (a -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
  TcM ReaderT RO (ExceptionT Error (StateT RW Id)) a
m >>= :: TcM a -> (a -> TcM b) -> TcM b
>>= a -> TcM b
f = ReaderT RO (ExceptionT Error (StateT RW Id)) b -> TcM b
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM (do a
a <- ReaderT RO (ExceptionT Error (StateT RW Id)) a
m
                        let TcM ReaderT RO (ExceptionT Error (StateT RW Id)) b
m1 = a -> TcM b
f a
a
                        ReaderT RO (ExceptionT Error (StateT RW Id)) b
m1)

runTcM :: InferInput -> TcM a -> Either Error (a, [ProofObligation])
runTcM :: InferInput -> TcM a -> Either Error (a, [Schema])
runTcM InferInput
env (TcM ReaderT RO (ExceptionT Error (StateT RW Id)) a
m) =
  case ReaderT RO (ExceptionT Error (StateT RW Id)) a
-> RO -> RW -> (Either Error a, RW)
forall (m :: * -> *) a r. RunM m a r => m a -> r
runM ReaderT RO (ExceptionT Error (StateT RW Id)) a
m RO
ro RW
rw of
    (Left Error
err, RW
_) -> Error -> Either Error (a, [Schema])
forall a b. a -> Either a b
Left Error
err
    (Right a
a, RW
s)  -> (a, [Schema]) -> Either Error (a, [Schema])
forall a b. b -> Either a b
Right (a
a, RW -> [Schema]
woProofObligations RW
s)
  where
  ro :: RO
ro = RO :: Map Int TParam -> [Prop] -> Map Name Schema -> 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 (InferInput -> Map Name ModTParam
inpParamTypes InferInput
env)
                                      , let x :: TParam
x = ModTParam -> TParam
mtpParam ModTParam
tp ]
          , roAsmps :: [Prop]
roAsmps = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing (InferInput -> [Located Prop]
inpParamConstraints InferInput
env)
          , roVars :: Map Name Schema
roVars  = Map Name Schema -> Map Name Schema -> Map Name Schema
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union
                        ((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (InferInput -> Map Name ModVParam
inpParamFuns InferInput
env))
                        (InferInput -> Map Name Schema
inpVars InferInput
env)
          }
  rw :: RW
rw = RW :: [Schema] -> 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
    deriving Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show

reportError :: Error -> TcM a
reportError :: Error -> TcM a
reportError Error
e = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM (Error -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise Error
e)

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

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

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

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

proofObligation :: Prop -> TcM ()
proofObligation :: Prop -> TcM ()
proofObligation Prop
p = ReaderT RO (ExceptionT Error (StateT RW Id)) () -> TcM ()
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT Error (StateT RW Id)) () -> TcM ())
-> ReaderT RO (ExceptionT Error (StateT RW Id)) () -> TcM ()
forall a b. (a -> b) -> a -> b
$
  do RO
ro <- ReaderT RO (ExceptionT Error (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     (RW -> RW) -> ReaderT RO (ExceptionT Error (StateT RW Id)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ ((RW -> RW) -> ReaderT RO (ExceptionT Error (StateT RW Id)) ())
-> (RW -> RW) -> ReaderT RO (ExceptionT Error (StateT RW Id)) ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { woProofObligations :: [Schema]
woProofObligations =
                             [TParam] -> [Prop] -> Prop -> Schema
Forall (Map Int TParam -> [TParam]
forall k a. Map k a -> [a]
Map.elems (RO -> Map Int TParam
roTVars RO
ro)) (RO -> [Prop]
roAsmps RO
ro) Prop
p
                           Schema -> [Schema] -> [Schema]
forall a. a -> [a] -> [a]
: RW -> [Schema]
woProofObligations RW
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 Error (StateT RW Id)) RO -> TcM RO
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT 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 (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 Error (StateT RW Id)) RO -> TcM RO
forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT 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 (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