module DDC.Core.Check.CheckExp
( Config (..)
, AnTEC (..)
, checkExp
, typeOfExp
, CheckM
, checkExpM
, TaggedClosure(..))
where
import DDC.Core.Predicates
import DDC.Core.Compounds
import DDC.Core.Collect
import DDC.Core.Pretty
import DDC.Core.Exp
import DDC.Core.Check.Error
import DDC.Core.Check.CheckDaCon
import DDC.Core.Check.CheckWitness
import DDC.Core.Check.TaggedClosure
import DDC.Type.Transform.SubstituteT
import DDC.Type.Transform.Crush
import DDC.Type.Transform.Trim
import DDC.Type.Transform.Instantiate
import DDC.Type.Transform.LiftT
import DDC.Type.DataDef
import DDC.Type.Equiv
import DDC.Type.Universe
import DDC.Type.Sum as Sum
import DDC.Type.Env (Env, KindEnv, TypeEnv)
import DDC.Control.Monad.Check (throw, result)
import Data.Set (Set)
import qualified DDC.Type.Env as Env
import qualified Data.Set as Set
import Control.Monad
import DDC.Data.ListUtils
import Data.List as L
import Data.Maybe
import Data.Typeable
import Control.DeepSeq
data AnTEC a n
= AnTEC
{ annotType :: (Type n)
, annotEffect :: (Effect n)
, annotClosure :: (Closure n)
, annotTail :: a }
deriving (Show, Typeable)
instance (NFData a, NFData n) => NFData (AnTEC a n) where
rnf !an
= rnf (annotType an)
`seq` rnf (annotEffect an)
`seq` rnf (annotClosure an)
`seq` rnf (annotTail an)
instance Pretty (AnTEC a n) where
ppr _ = text "AnTEC"
checkExp
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Exp a n
-> Either (Error a n)
( Exp (AnTEC a n) n
, Type n
, Effect n
, Closure n)
checkExp !config !kenv !tenv !xx
= result
$ do (xx', t, effs, clos)
<- checkExpM config
(Env.union kenv (configPrimKinds config))
(Env.union tenv (configPrimTypes config))
xx
return ( xx'
, t
, TSum effs
, closureOfTaggedSet clos)
typeOfExp
:: (Ord n, Pretty n, Show n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Exp a n
-> Either (Error a n) (Type n)
typeOfExp !config !kenv !tenv !xx
= case checkExp config kenv tenv xx of
Left err -> Left err
Right (_, t, _, _) -> Right t
checkExpM
:: (Show n, Pretty n, Ord n)
=> Config n
-> Env n
-> Env n
-> Exp a n
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, TypeSum n
, Set (TaggedClosure n))
checkExpM !config !kenv !tenv !xx
=
checkExpM' config kenv tenv xx
checkExpM' !_config !_kenv !tenv (XVar a u)
= case Env.lookup u tenv of
Nothing -> throw $ ErrorUndefinedVar u UniverseData
Just t
-> returnX a
(\z -> XVar z u)
t
(Sum.empty kEffect)
(Set.singleton $ taggedClosureOfValBound t u)
checkExpM' !config !_kenv !_tenv xx@(XCon a dc)
= do
when (isBot $ daConType dc)
$ throw $ ErrorUndefinedCtor xx
checkDaConM config xx dc
let tResult
= typeOfDaCon dc
returnX a
(\z -> XCon z dc)
tResult
(Sum.empty kEffect)
Set.empty
checkExpM' !config !kenv !tenv xx@(XApp a x1 (XType t2))
= do (x1', t1, effs1, clos1) <- checkExpM config kenv tenv x1
k2 <- checkTypeM config kenv t2
let Just t2_clo = taggedClosureOfTyArg kenv t2
case t1 of
TForall b11 t12
| typeOfBind b11 == k2
-> returnX a
(\z -> XApp z x1' (XType t2))
(substituteT b11 t2 t12)
effs1
(clos1 `Set.union` t2_clo)
| otherwise -> throw $ ErrorAppMismatch xx (typeOfBind b11) t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' !config !kenv !tenv xx@(XApp a x1 (XWitness w2))
= do (x1', t1, effs1, clos1) <- checkExpM config kenv tenv x1
t2 <- checkWitnessM config kenv tenv w2
case t1 of
TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
| t11 `equivT` t2
-> returnX a
(\z -> XApp z x1' (XWitness w2))
t12 effs1 clos1
| otherwise -> throw $ ErrorAppMismatch xx t11 t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' !config !kenv !tenv xx@(XApp a x1 x2)
= do (x1', t1, effs1, clos1) <- checkExpM config kenv tenv x1
(x2', t2, effs2, clos2) <- checkExpM config kenv tenv x2
case t1 of
TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12
| t11 `equivT` t2
, effs <- Sum.fromList kEffect [eff]
-> returnX a
(\z -> XApp z x1' x2')
t12
(effs1 `Sum.union` effs2 `Sum.union` effs)
(clos1 `Set.union` clos2)
| otherwise -> throw $ ErrorAppMismatch xx t11 t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' !config !kenv !tenv xx@(XLAM a b1 x2)
= do let t1 = typeOfBind b1
_ <- checkTypeM config kenv t1
let kenv' = Env.extend b1 kenv
let tenv' = Env.lift 1 tenv
(x2', t2, e2, c2) <- checkExpM config kenv' tenv' x2
k2 <- checkTypeM config kenv' t2
when (Env.memberBind b1 kenv)
$ throw $ ErrorLamShadow xx b1
when (e2 /= Sum.empty kEffect)
$ throw $ ErrorLamNotPure xx True (TSum e2)
when (not $ isDataKind k2)
$ throw $ ErrorLamBodyNotData xx b1 t2 k2
let c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureT b1)
$ Set.toList c2
returnX a
(\z -> XLAM z b1 x2')
(TForall b1 t2)
(Sum.empty kEffect)
c2_cut
checkExpM' !config !kenv !tenv xx@(XLam a b1 x2)
= do
let t1 = typeOfBind b1
k1 <- checkTypeM config kenv t1
let tenv' = Env.extend b1 tenv
(x2', t2, e2, c2) <- checkExpM config kenv tenv' x2
k2 <- checkTypeM config kenv t2
case universeFromType2 k1 of
Just UniverseData
| not $ isDataKind k1
-> throw $ ErrorLamBindNotData xx t1 k1
| not $ isDataKind k2
-> throw $ ErrorLamBodyNotData xx b1 t2 k2
| otherwise
-> let
c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureX b1)
$ Set.toList c2
Just c2_captured
| configSuppressClosures config
= Just $ tBot kClosure
| otherwise
= trimClosure $ closureOfTaggedSet c2_cut
in returnX a
(\z -> XLam z b1 x2')
(tFun t1 (TSum e2) c2_captured t2)
(Sum.empty kEffect)
c2_cut
Just UniverseWitness
| e2 /= Sum.empty kEffect
-> throw $ ErrorLamNotPure xx False (TSum e2)
| not $ isDataKind k2
-> throw $ ErrorLamBodyNotData xx b1 t2 k2
| otherwise
-> returnX a
(\z -> XLam z b1 x2')
(tImpl t1 t2)
(Sum.empty kEffect)
c2
_ -> throw $ ErrorMalformedType xx k1
checkExpM' !config !kenv !tenv xx@(XLet a lts x2)
| case lts of
LLet{} -> True
LRec{} -> True
_ -> False
= do
(lts', bs', effs12, clo12)
<- checkLetsM xx config kenv tenv lts
let tenv1 = Env.extends bs' tenv
(x2', t2, effs2, c2) <- checkExpM config kenv tenv1 x2
k2 <- checkTypeM config kenv t2
when (not $ isDataKind k2)
$ throw $ ErrorLetBodyNotData xx t2 k2
let c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureXs bs')
$ Set.toList c2
returnX a
(\z -> XLet z lts' x2')
t2
(effs12 `Sum.union` effs2)
(clo12 `Set.union` c2_cut)
checkExpM' !config !kenv !tenv xx@(XLet a (LLetRegions bsRgn bsWit) x)
= case takeSubstBoundsOfBinds bsRgn of
[] -> checkExpM config kenv tenv x
us -> do
let depth = length $ map isBAnon bsRgn
let ks = map typeOfBind bsRgn
mapM_ (checkTypeM config kenv) ks
when (any (not . isRegionKind) ks)
$ throw $ ErrorLetRegionsNotRegion xx bsRgn ks
let rebounds = filter (flip Env.memberBind kenv) bsRgn
when (not $ null rebounds)
$ throw $ ErrorLetRegionsRebound xx rebounds
let kenv' = Env.extends bsRgn kenv
let tenv' = Env.lift depth tenv
mapM_ (checkTypeM config kenv') $ map typeOfBind bsWit
checkWitnessBindsM kenv xx us bsWit
let tenv2 = Env.extends bsWit tenv'
(xBody', tBody, effs, clo) <- checkExpM config kenv' tenv2 x
kBody <- checkTypeM config kenv' tBody
when (not $ isDataKind kBody)
$ throw $ ErrorLetBodyNotData xx tBody kBody
let fvsT = freeT Env.empty tBody
when (any (flip Set.member fvsT) us)
$ throw $ ErrorLetRegionFree xx bsRgn tBody
let delEff es u = Sum.delete (tRead (TVar u))
$ Sum.delete (tWrite (TVar u))
$ Sum.delete (tAlloc (TVar u))
$ es
let effs' = foldl delEff effs us
let cutClo c r = mapMaybe (cutTaggedClosureT r) c
let c2_cut = Set.fromList
$ foldl cutClo (Set.toList clo) bsRgn
returnX a
(\z -> XLet z (LLetRegions bsRgn bsWit) xBody')
(lowerT depth tBody)
(lowerT depth effs')
c2_cut
checkExpM' !config !kenv !tenv xx@(XLet a (LWithRegion u) x)
= do
(case Env.lookup u kenv of
Nothing -> throw $ ErrorUndefinedVar u UniverseSpec
Just k | not $ isRegionKind k
-> throw $ ErrorWithRegionNotRegion xx u k
_ -> return ())
(xBody', tBody, effs, clo)
<- checkExpM config kenv tenv x
kBody <- checkTypeM config kenv tBody
when (not $ isDataKind kBody)
$ throw $ ErrorLetBodyNotData xx tBody kBody
let tcs = supportTyCon
$ support Env.empty Env.empty tBody
when (Set.member u tcs)
$ throw $ ErrorWithRegionFree xx u tBody
let tu = TCon $ TyConBound u kRegion
let effs' = Sum.delete (tRead tu)
$ Sum.delete (tWrite tu)
$ Sum.delete (tAlloc tu)
$ effs
let clo_masked = Set.delete (GBoundRgnCon u) clo
returnX a
(\z -> XLet z (LWithRegion u) xBody')
tBody
effs'
clo_masked
checkExpM' !config !kenv !tenv xx@(XCase a xDiscrim alts)
= do
(xDiscrim', tDiscrim, effsDiscrim, closDiscrim)
<- checkExpM config kenv tenv xDiscrim
(mmode, tsArgs)
<- case takeTyConApps tDiscrim of
Just (tc, ts)
| TyConSpec TcConUnit <- tc
-> return ( Just (DataModeSmall [])
, [] )
| TyConBound (UName nTyCon) k <- tc
, takeResultKind k == kData
-> return ( lookupModeOfDataType nTyCon (configPrimDataDefs config)
, ts )
| TyConBound (UPrim nTyCon _) k <- tc
, takeResultKind k == kData
-> return ( lookupModeOfDataType nTyCon (configPrimDataDefs config)
, ts )
_ -> throw $ ErrorCaseScrutineeNotAlgebraic xx tDiscrim
mode
<- case mmode of
Nothing -> throw $ ErrorCaseScrutineeTypeUndeclared xx tDiscrim
Just m -> return m
(alts', ts, effss, closs)
<- liftM unzip4
$ mapM (checkAltM xx config kenv tenv tDiscrim tsArgs) alts
when (null ts)
$ throw $ ErrorCaseNoAlternatives xx
let (tAlt : _) = ts
forM_ ts $ \tAlt'
-> when (not $ equivT tAlt tAlt')
$ throw $ ErrorCaseAltResultMismatch xx tAlt tAlt'
let pats = [p | AAlt p _ <- alts]
let psDefaults = filter isPDefault pats
let nsCtorsMatched = mapMaybe takeCtorNameOfAlt alts
when (length psDefaults > 1)
$ throw $ ErrorCaseOverlapping xx
when (length (nub nsCtorsMatched) /= length nsCtorsMatched )
$ throw $ ErrorCaseOverlapping xx
(case pats of
[] -> throw $ ErrorCaseNoAlternatives xx
_ | Just patsInit <- takeInit pats
, or $ map isPDefault $ patsInit
-> throw $ ErrorCaseOverlapping xx
| otherwise
-> return ())
(case mode of
DataModeSmall nsCtors
| any isPDefault [p | AAlt p _ <- alts]
-> return ()
| nsCtorsMissing <- nsCtors \\ nsCtorsMatched
, not $ null nsCtorsMissing
-> throw $ ErrorCaseNonExhaustive xx nsCtorsMissing
| otherwise
-> return ()
DataModeLarge
| any isPDefault [p | AAlt p _ <- alts] -> return ()
| otherwise
-> throw $ ErrorCaseNonExhaustiveLarge xx)
let effsMatch
= Sum.singleton kEffect
$ crushEffect $ tHeadRead tDiscrim
returnX a
(\z -> XCase z xDiscrim' alts')
tAlt
(Sum.unions kEffect (effsDiscrim : effsMatch : effss))
(Set.unions (closDiscrim : closs))
checkExpM' !config !kenv !tenv xx@(XCast a (CastWeakenEffect eff) x1)
= do
kEff <- checkTypeM config kenv eff
when (not $ isEffectKind kEff)
$ throw $ ErrorWeakEffNotEff xx eff kEff
(x1', t1, effs, clo) <- checkExpM config kenv tenv x1
let c' = CastWeakenEffect eff
returnX a
(\z -> XCast z c' x1')
t1
(Sum.insert eff effs)
clo
checkExpM' !config !kenv !tenv (XCast a (CastWeakenClosure xs) x1)
= do
(xs', closs)
<- liftM unzip
$ mapM (checkArgM config kenv tenv) xs
(x1', t1, effs, clos) <- checkExpM config kenv tenv x1
let c' = CastWeakenClosure xs'
returnX a
(\z -> XCast z c' x1')
t1
effs
(Set.unions (clos : closs))
checkExpM' !config !kenv !tenv xx@(XCast a (CastPurify w) x1)
= do
tW <- checkWitnessM config kenv tenv w
(x1', t1, effs, clo) <- checkExpM config kenv tenv x1
effs' <- case tW of
TApp (TCon (TyConWitness TwConPure)) effMask
-> return $ Sum.delete effMask effs
_ -> throw $ ErrorWitnessNotPurity xx w tW
let c' = CastPurify w
returnX a
(\z -> XCast z c' x1')
t1 effs' clo
checkExpM' !config !kenv !tenv xx@(XCast a (CastForget w) x1)
= do
tW <- checkWitnessM config kenv tenv w
(x1', t1, effs, clos) <- checkExpM config kenv tenv x1
clos' <- case tW of
TApp (TCon (TyConWitness TwConEmpty)) cloMask
-> return $ maskFromTaggedSet
(Sum.singleton kClosure cloMask)
clos
_ -> throw $ ErrorWitnessNotEmpty xx w tW
let c' = CastForget w
returnX a
(\z -> XCast z c' x1')
t1 effs clos'
checkExpM' !_config !_kenv !_tenv xx@(XType _)
= throw $ ErrorNakedType xx
checkExpM' !_config !_kenv !_tenv xx@(XWitness _)
= throw $ ErrorNakedWitness xx
checkExpM' _ _ _ _
= error "checkExpM: bogus warning killer"
checkArgM
:: (Show n, Pretty n, Ord n)
=> Config n
-> Env n
-> Env n
-> Exp a n
-> CheckM a n
( Exp (AnTEC a n) n
, Set (TaggedClosure n))
checkArgM !config !kenv !tenv !xx
= case xx of
XType t
-> do checkTypeM config kenv t
let Just clo = taggedClosureOfTyArg kenv t
return ( XType t
, clo)
XWitness w
-> do checkWitnessM config kenv tenv w
return ( XWitness w
, Set.empty)
_ -> do
(xx', _, _, clos) <- checkExpM config kenv tenv xx
return ( xx'
, clos)
returnX :: Ord n
=> a
-> (AnTEC a n -> Exp (AnTEC a n) n)
-> Type n
-> TypeSum n
-> Set (TaggedClosure n)
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, TypeSum n
, Set (TaggedClosure n))
returnX !a !f !t !es !cs
= let e = TSum es
c = closureOfTaggedSet cs
in return (f (AnTEC t e c a)
, t, es, cs)
checkLetsM
:: (Show n, Pretty n, Ord n)
=> Exp a n
-> Config n
-> Env n
-> Env n
-> Lets a n
-> CheckM a n
( Lets (AnTEC a n) n
, [Bind n]
, TypeSum n
, Set (TaggedClosure n))
checkLetsM !xx !config !kenv !tenv (LLet mode b11 x12)
= do
(x12', t12, effs12, clo12)
<- checkExpM config kenv tenv x12
(b11', k11')
<- checkLetBindOfTypeM xx config kenv tenv t12 b11
when (not $ isDataKind k11')
$ throw $ ErrorLetBindingNotData xx b11' k11'
(case mode of
LetStrict -> return ()
LetLazy _
-> do let eff12' = TSum effs12
when (not $ isBot eff12')
$ throw $ ErrorLetLazyNotPure xx b11 eff12'
let clo12' = closureOfTaggedSet clo12
when (not $ isBot clo12')
$ throw $ ErrorLetLazyNotEmpty xx b11 clo12')
(case mode of
LetStrict -> return ()
LetLazy Nothing
-> do case takeDataTyConApps t12 of
Just (_tc, t1 : _)
-> do k1 <- checkTypeM config kenv t1
when (isRegionKind k1)
$ throw $ ErrorLetLazyNoWitness xx b11 t12
_ -> return ()
LetLazy (Just wit)
-> do tWit <- checkWitnessM config kenv tenv wit
let tWitExp = case takeDataTyConApps t12 of
Just (_tc, tR : _ts) -> tLazy tR
_ -> tHeadLazy t12
when (not $ equivT tWit tWitExp)
$ throw $ ErrorLetLazyWitnessTypeMismatch
xx b11 tWit t12 tWitExp)
return ( LLet mode b11' x12'
, [b11']
, effs12
, clo12)
checkLetsM !xx !config !kenv !tenv (LRec bxs)
= do
let (bs, xs) = unzip bxs
(case duplicates $ filter isBName bs of
[] -> return ()
b : _ -> throw $ ErrorLetrecRebound xx b)
ks <- mapM (checkTypeM config kenv)
$ map typeOfBind bs
zipWithM_ (\b k
-> when (not $ isDataKind k)
$ throw $ ErrorLetBindingNotData xx b k)
bs ks
forM_ xs $ \x
-> when (not $ (isXLam x || isXLAM x))
$ throw $ ErrorLetrecBindingNotLambda xx x
let tenv' = Env.extends bs tenv
(xsRight', tsRight, _effssBinds, clossBinds)
<- liftM unzip4 $ mapM (checkExpM config kenv tenv') xs
zipWithM_ (\b t
-> if not $ equivT (typeOfBind b) t
then throw $ ErrorLetMismatch xx b t
else return ())
bs tsRight
let clos_cut
= Set.fromList
$ mapMaybe (cutTaggedClosureXs bs)
$ Set.toList
$ Set.unions clossBinds
return ( LRec (zip bs xsRight')
, zipWith replaceTypeOfBind tsRight bs
, Sum.empty kEffect
, clos_cut)
checkLetsM _xx _config _kenv _tenv _lts
= error "checkLetsM: case should have been handled in checkExpM"
duplicates :: Eq a => [a] -> [a]
duplicates [] = []
duplicates (x : xs)
| L.elem x xs = x : duplicates (filter (/= x) xs)
| otherwise = duplicates xs
checkAltM
:: (Show n, Pretty n, Ord n)
=> Exp a n
-> Config n
-> Env n
-> Env n
-> Type n
-> [Type n]
-> Alt a n
-> CheckM a n
( Alt (AnTEC a n) n
, Type n
, TypeSum n
, Set (TaggedClosure n))
checkAltM !_xx !config !kenv !tenv !_tDiscrim !_tsArgs (AAlt PDefault xBody)
= do (xBody', tBody, effBody, cloBody)
<- checkExpM config kenv tenv xBody
return ( AAlt PDefault xBody'
, tBody
, effBody
, cloBody)
checkAltM !xx !config !kenv !tenv !tDiscrim !tsArgs (AAlt (PData dc bsArg) xBody)
= do
let Just aCase = takeAnnotOfExp xx
(if isBot (daConType dc)
then throw $ ErrorUndefinedCtor $ XCon aCase dc
else return ())
let tCtor = daConType dc
tCtor_inst
<- case instantiateTs tCtor tsArgs of
Nothing -> throw $ ErrorCaseCannotInstantiate xx tDiscrim tCtor
Just t -> return t
let (tsFields_ctor, tResult)
= takeTFunArgResult tCtor_inst
when (not $ equivT tDiscrim tResult)
$ throw $ ErrorCaseScrutineeTypeMismatch xx tDiscrim tResult
when (length tsFields_ctor < length bsArg)
$ throw $ ErrorCaseTooManyBinders xx dc
(length tsFields_ctor)
(length bsArg)
tsFields <- zipWithM (mergeAnnot xx)
(map typeOfBind bsArg)
tsFields_ctor
let bsArg' = zipWith replaceTypeOfBind tsFields bsArg
let tenv' = Env.extends bsArg' tenv
(xBody', tBody, effsBody, closBody)
<- checkExpM config kenv tenv' xBody
let closBody_cut
= Set.fromList
$ mapMaybe (cutTaggedClosureXs bsArg')
$ Set.toList closBody
return ( AAlt (PData dc bsArg') xBody'
, tBody
, effsBody
, closBody_cut)
mergeAnnot :: Eq n => Exp a n -> Type n -> Type n -> CheckM a n (Type n)
mergeAnnot !xx !tAnnot !tActual
| isBot tAnnot = return tActual
| tAnnot == tActual = return tActual
| otherwise
= throw $ ErrorCaseFieldTypeMismatch xx tAnnot tActual
checkWitnessBindsM
:: (Show n, Ord n)
=> KindEnv n
-> Exp a n
-> [Bound n]
-> [Bind n]
-> CheckM a n ()
checkWitnessBindsM !kenv !xx !nRegions !bsWits
= mapM_ (checkWitnessBindM kenv xx nRegions bsWits) bsWits
checkWitnessBindM
:: (Show n, Ord n)
=> Env n
-> Exp a n
-> [Bound n]
-> [Bind n]
-> Bind n
-> CheckM a n ()
checkWitnessBindM !kenv !xx !uRegions !bsWit !bWit
= let btsWit
= [(typeOfBind b, b) | b <- bsWit]
checkWitnessArg t
= case t of
TVar u'
| all (/= u') uRegions -> throw $ ErrorLetRegionsWitnessOther xx uRegions bWit
| otherwise -> return ()
TCon (TyConBound u' _)
| all (/= u') uRegions -> throw $ ErrorLetRegionsWitnessOther xx uRegions bWit
| otherwise -> return ()
_ -> throw $ ErrorLetRegionWitnessInvalid xx bWit
inEnv t
= case t of
TVar u' | Env.member u' kenv -> True
TCon (TyConBound u' _) | Env.member u' kenv -> True
_ -> False
in case typeOfBind bWit of
TApp (TCon (TyConWitness TwConGlobal)) t2
-> checkWitnessArg t2
TApp (TCon (TyConWitness TwConConst)) t2
| Just bConflict <- L.lookup (tMutable t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConMutable)) t2
| Just bConflict <- L.lookup (tConst t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConLazy)) t2
| Just bConflict <- L.lookup (tManifest t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConManifest)) t2
| Just bConflict <- L.lookup (tLazy t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
(takeTyConApps -> Just (TyConWitness (TwConDistinct 2), [t1, t2]))
| inEnv t1 -> checkWitnessArg t2
| inEnv t2 -> checkWitnessArg t1
| t1 /= t2 -> mapM_ checkWitnessArg [t1, t2]
| otherwise -> throw $ ErrorLetRegionWitnessInvalid xx bWit
(takeTyConApps -> Just (TyConWitness (TwConDistinct _), ts))
-> mapM_ checkWitnessArg ts
_ -> throw $ ErrorLetRegionWitnessInvalid xx bWit
checkLetBindOfTypeM
:: (Ord n, Show n, Pretty n)
=> Exp a n
-> Config n
-> Env n
-> Env n
-> Type n
-> Bind n
-> CheckM a n (Bind n, Kind n)
checkLetBindOfTypeM !xx !config !kenv !_tenv !tRight b
| isBot (typeOfBind b)
= do k <- checkTypeM config kenv tRight
return ( replaceTypeOfBind tRight b
, k)
| not $ equivT (typeOfBind b) tRight
= throw $ ErrorLetMismatch xx b tRight
| otherwise
= do k <- checkTypeM config kenv (typeOfBind b)
return (b, k)