-- |
-- 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, singleSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.Utils.Ident

import qualified Data.Set as Set
import Data.List (sort, sortBy)
import Data.Function (on)
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 env :: InferInput
env e :: 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 env :: InferInput
env ds0 :: [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 err :: Error
err     -> Error -> Either Error [Schema]
forall a b. a -> Either a b
Left Error
err
                    Right (_,ps :: [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 env :: InferInput
env m :: Module
m = case InferInput -> TcM () -> Either Error ((), [Schema])
forall a. InferInput -> TcM a -> Either Error (a, [Schema])
runTcM InferInput
env TcM ()
check of
                   Left err :: Error
err -> Error -> Either Error [Schema]
forall a b. a -> Either a b
Left Error
err
                   Right (_,ps :: [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 decls :: [DeclGroup]
decls =
  case [DeclGroup]
decls of
    [] -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    d :: DeclGroup
d : ds :: [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 ty :: Prop
ty =
  case Prop
ty of
    TUser _ _ t :: Prop
t -> Prop -> TcM Kind
checkType Prop
t    -- Maybe check synonym too?

    TCon tc :: TCon
tc ts :: [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 tv :: TVar
tv -> TVar -> TcM Kind
lookupTVar TVar
tv

    TRec fs :: [(Ident, Prop)]
fs ->
      do [(Ident, Prop)] -> ((Ident, Prop) -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Ident, Prop)]
fs (((Ident, Prop) -> TcM ()) -> TcM ())
-> ((Ident, Prop) -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \(_,t :: 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 k :: Kind
k [] = case Kind
k of
                     _ :-> _  -> 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
                     KProp    -> Kind -> TcM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     KNum     -> Kind -> TcM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                     KType    -> Kind -> TcM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k

  checkKind (k1 :: Kind
k1 :-> k2 :: Kind
k2) (k :: Kind
k : ks :: [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 k :: Kind
k ks :: [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 k :: Kind
k ty :: 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 as :: [TParam]
as ps :: [Prop]
ps t :: 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 (x :: a
x : xs :: [a]
xs) (y :: a
y : ys :: [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 _ _ = Bool
False

instance Same Type where
  same :: Prop -> Prop -> Bool
same t1 :: Prop
t1 t2 :: 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 xs :: [TParam]
xs ps :: [Prop]
ps s :: Prop
s) (Forall ys :: [TParam]
ys qs :: [Prop]
qs t :: 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 x :: TParam
x y :: 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
expr =
  do Schema
s <- Expr -> TcM Schema
exprSchema Expr
expr
     case Schema -> Maybe Prop
isMono Schema
s of
       Just t :: Prop
t  -> Prop -> TcM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t
       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
expr =
  case Expr
expr of

    EList es :: [Expr]
es t :: 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
$ \e :: 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 "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 es :: [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 fs :: [(Ident, Expr)]
fs ->
      do [(Ident, Prop)]
fs1 <- [(Ident, Expr)]
-> ((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ident, Expr)]
fs (((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)])
-> ((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)]
forall a b. (a -> b) -> a -> b
$ \(f :: Ident
f,e :: Expr
e) -> do Prop
t <- Expr -> TcM Prop
exprType Expr
e
                                       (Ident, Prop) -> TcM (Ident, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
f,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
$ Prop -> Schema
tMono (Prop -> Schema) -> Prop -> Schema
forall a b. (a -> b) -> a -> b
$ [(Ident, Prop)] -> Prop
TRec [(Ident, Prop)]
fs1

    ESet e :: Expr
e x :: Selector
x v :: 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 "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 e :: Expr
e sel :: 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 e1 :: Expr
e1 e2 :: Expr
e2 e3 :: 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 "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 "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 len :: Prop
len t :: Prop
t e :: Expr
e mss :: [[Match]]
mss ->
      do Kind -> Prop -> TcM ()
checkTypeIs Kind
KNum Prop
len
         Kind -> Prop -> TcM ()
checkTypeIs Kind
KType Prop
t

         (xs :: [[(Name, Schema)]]
xs,ls :: [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 -> 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 x :: Name
x -> Name -> TcM Schema
lookupVar Name
x

    ETAbs a :: TParam
a e :: Expr
e     ->
      do Forall as :: [TParam]
as p :: [Prop]
p t :: 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 e :: Expr
e t :: Prop
t ->
      do Kind
k <- Prop -> TcM Kind
checkType Prop
t
         Schema
s <- Expr -> TcM Schema
exprSchema Expr
e
         case Schema
s of
           Forall (a :: TParam
a : as :: [TParam]
as) ps :: [Prop]
ps t1 :: 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
$ \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 = TVar -> Prop -> Subst
singleSubst (TParam -> TVar
tpVar 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 [] _ _ -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadInstantiation

    EApp e1 :: Expr
e1 e2 :: 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 TCFun) [ a :: Prop
a, b :: 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)
           tf :: Prop
tf -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Prop -> Prop -> Error
BadApplication Prop
tf Prop
t1)


    EAbs x :: Name
x t :: Prop
t e :: 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 p :: Prop
p e :: 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 as :: [TParam]
as ps :: [Prop]
ps t :: 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 e :: Expr
e ->
      do Forall as :: [TParam]
as ps :: [Prop]
ps t :: Prop
t <- Expr -> TcM Schema
exprSchema Expr
e
         case ([TParam]
as,[Prop]
ps) of
           ([], p :: Prop
p:qs :: [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)
           ([], _)    -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadProofNoAbs
           (_,_)      -> Error -> TcM Schema
forall a. Error -> TcM a
reportError ([TParam] -> Error
BadProofTyVars [TParam]
as)


    -- XXX: Check that defined things are distinct?
    EWhere e :: Expr
e dgs :: [DeclGroup]
dgs ->
      let go :: [DeclGroup] -> TcM Schema
go []       = Expr -> TcM Schema
exprSchema Expr
e
          go (d :: DeclGroup
d : ds :: [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 t :: Prop
t sel :: Selector
sel =
  case Selector
sel of

    TupleSel n :: Int
n mb :: Maybe Int
mb ->

      case Prop -> Prop
tNoUser Prop
t of
        TCon (TC (TCTuple sz :: Int
sz)) ts :: [Prop]
ts ->
          do case Maybe Int
mb of
               Just sz1 :: 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))
               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 TCSeq) [s :: Prop
s,elT :: 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 TCFun) [a :: Prop
a,b :: 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])

        _ -> 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 f :: Ident
f mb :: Maybe [Ident]
mb ->
      case Prop -> Prop
tNoUser Prop
t of
        TRec fs :: [(Ident, Prop)]
fs ->

          do case Maybe [Ident]
mb of
               Nothing -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just fs1 :: [Ident]
fs1 ->
                 do let ns :: [Ident]
ns  = [Ident] -> [Ident]
forall a. Ord a => [a] -> [a]
sort (((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Ident
forall a b. (a, b) -> a
fst [(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 -> [(Ident, Prop)] -> Maybe Prop
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f [(Ident, Prop)]
fs of
               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
$ ((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Prop)]
fs
               Just ft :: Prop
ft -> Prop -> TcM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
ft

        TCon (TC TCSeq) [s :: Prop
s,elT :: 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 TCFun) [a :: Prop
a,b :: 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])


        _ -> 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 _ mb :: Maybe Int
mb ->
      case Prop -> Prop
tNoUser Prop
t of
        TCon (TC TCSeq) [ n :: Prop
n, elT :: Prop
elT ] ->

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

        _ -> 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 t1 :: Prop
t1 t2 :: 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 t1 :: Prop
t1 t2 :: Prop
t2 = Prop -> Prop -> TcM ()
go Prop
t1 Prop
t2
  where
  go :: Prop -> Prop -> TcM ()
go ty1 :: Prop
ty1 ty2 :: 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 "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 (x :: Prop
x : xs :: [Prop]
xs) (y :: Prop
y : ys :: [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 _ _               = TcM ()
forall a. TcM a
err

    in case Prop
ty1 of
         TUser _ _ s :: Prop
s   -> Prop -> Prop -> TcM ()
go Prop
s Prop
ty2

         TVar x :: TVar
x        -> case Prop
other of
                            TVar y :: 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 ()
                            _                -> TcM ()
forall a. TcM a
err

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

         TRec fs :: [(Ident, Prop)]
fs ->
           case Prop
other of
             TRec gs :: [(Ident, Prop)]
gs ->
               do let order :: [(Ident, b)] -> [(Ident, b)]
order = ((Ident, b) -> (Ident, b) -> Ordering)
-> [(Ident, b)] -> [(Ident, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Ident -> Ident -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Ident -> Ident -> Ordering)
-> ((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Ident, b) -> Ident
forall a b. (a, b) -> a
fst)
                      fs1 :: [(Ident, Prop)]
fs1   = [(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
order [(Ident, Prop)]
fs
                      gs1 :: [(Ident, Prop)]
gs1   = [(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
order [(Ident, Prop)]
gs
                  Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Prop)]
fs1 [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== ((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Prop)]
gs1) TcM ()
forall a. TcM a
err
                  [Prop] -> [Prop] -> TcM ()
goMany (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Prop
forall a b. (a, b) -> b
snd [(Ident, Prop)]
fs1) (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Prop
forall a b. (a, b) -> b
snd [(Ident, Prop)]
gs1)
             _ -> 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 checkSig :: Bool
checkSig d :: Decl
d =
  case Decl -> DeclDef
dDefinition Decl
d of

    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 e :: 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 "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 dg :: DeclGroup
dg =
  case DeclGroup
dg of
    NonRecursive d :: 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 ds :: [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
$ \d :: 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 ma :: Match
ma =
  case Match
ma of
    From x :: Name
x len :: Prop
len elt :: Prop
elt e :: 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 TCSeq) [ l :: Prop
l, el :: 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 "From" (Prop -> Schema
tMono Prop
elt) (Prop -> Schema
tMono Prop
el)


           _ -> 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 d :: 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 (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 [m :: Match
m]  = do (x :: (Name, Schema)
x,l :: 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 (m :: Match
m : ms :: [Match]
ms) =
  do (x :: (Name, Schema)
x, l :: Prop
l)   <- Match -> TcM ((Name, Schema), Prop)
checkMatch Match
m
     (xs :: [(Name, Schema)]
xs, l1 :: 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
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 m :: ReaderT RO (ExceptionT Error (StateT RW Id)) a
m >>= :: TcM a -> (a -> TcM b) -> TcM b
>>= f :: 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 m1 :: 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 env :: InferInput
env (TcM m :: 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 err :: Error
err, _) -> Error -> Either Error (a, [Schema])
forall a b. a -> Either a b
Left Error
err
    (Right a :: a
a, s :: 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 e :: 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 a :: TParam
a (TcM m :: 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 p :: Prop
p (TcM m :: 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 x :: Name
x t :: 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 xs :: [(Name, Schema)]
xs (TcM m :: 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 p :: 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
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 x :: TVar
x =
  case TVar
x of
    TVFree {} -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (TVar -> Error
FreeTypeVariable TVar
x)
    TVBound tpv :: 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 tp :: 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
            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 x :: 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 s :: Schema
s -> Schema -> TcM Schema
forall (m :: * -> *) a. Monad m => a -> m a
return Schema
s
       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