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


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

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

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

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

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

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


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

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

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

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

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

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

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

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

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


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

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

data AreSame = SameIf [Prop]
             | NotSame

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

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

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

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

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




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

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

data Field a b = Field a b

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

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

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

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





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


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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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


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


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

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


    EPropGuards [([Type], Expr)]
_guards Type
typ -> 
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Forall {sVars :: [TParam]
sVars = [], sProps :: [Type]
sProps = [], sType :: Type
sType = Type
typ}

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

    TupleSel Int
n Maybe Int
mb ->

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

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

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

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


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

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

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

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

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


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


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

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

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

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




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

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

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

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

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

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

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

         TRec RecordMap Ident Type
fs ->
           case Type
other of
             TRec RecordMap Ident Type
gs ->
               do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs forall a. Eq a => a -> a -> Bool
== forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
gs) forall {a}. TcM a
err
                  [Type] -> [Type] -> TcM ()
goMany (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs) (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
gs)
             Type
_ -> 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 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
         forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)

    DForeign FFIFunType
_ ->
      do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
         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
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema Schema
s
         Schema
s1 <- Expr -> TcM Schema
exprSchema Expr
e
         let nm :: Name
nm = Decl -> Name
dName Decl
d
             loc :: String
loc = String
"definition of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Name
nm) forall a. [a] -> [a] -> [a]
++
                            String
", at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
nm))
         String -> Schema -> Schema -> TcM ()
sameSchemas String
loc Schema
s Schema
s1

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


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

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

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




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

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

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

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

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

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

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

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

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

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


data Error =
    TypeMismatch String Schema Schema    -- ^ expected, actual
  | ExpectedMono Schema           -- ^ expected a mono type, got this
  | TupleSelectorOutOfRange Int Int
  | MissingField Ident [Ident]
  | UnexpectedTupleShape Int Int
  | UnexpectedRecordShape [Ident] [Ident]
  | UnexpectedSequenceShape Int Type
  | BadSelector Selector Type
  | BadInstantiation
  | Captured TVar
  | BadProofNoAbs
  | BadProofTyVars [TParam]
  | KindMismatch Kind Kind
  | NotEnoughArgumentsInKind Kind
  | BadApplication Type Type
  | FreeTypeVariable TVar
  | BadTypeApplication Kind [Kind]
  | RepeatedVariableInForall TParam
  | BadMatch Type
  | EmptyArm
  | UndefinedTypeVaraible TVar
  | UndefinedVariable Name
    deriving Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
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 :: forall a. Error -> TcM a
reportError Error
e = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise (RO -> Range
roRange RO
ro, Error
e)

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

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

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

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

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

proofObligation :: Prop -> TcM ()
proofObligation :: Type -> TcM ()
proofObligation Type
p = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { woProofObligations :: [Schema]
woProofObligations =
                             [TParam] -> [Type] -> Type -> Schema
Forall (forall k a. Map k a -> [a]
Map.elems (RO -> Map Int TParam
roTVars RO
ro)) (RO -> [Type]
roAsmps RO
ro) Type
p
                           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 {} -> 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 <- forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall (m :: * -> *) i. ReaderM m i => m i
ask
          case 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
              | forall t. HasKind t => t -> Kind
kindOf TParam
tp forall a. Eq a => a -> a -> Bool
== Kind
k  -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
              | Bool
otherwise       -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch (forall t. HasKind t => t -> Kind
kindOf TParam
tp) Kind
k
            Maybe TParam
Nothing  -> forall a. Error -> TcM a
reportError 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 <- forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall (m :: * -> *) i. ReaderM m i => m i
ask
     case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Schema
s
       Maybe Schema
Nothing -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Name -> Error
UndefinedVariable Name
x


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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