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.Annot.AnTEC
import DDC.Core.Check.Error
import DDC.Core.Check.CheckDaCon
import DDC.Core.Check.CheckWitness
import DDC.Core.Check.TaggedClosure
import DDC.Core.Transform.Reannotate
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
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
(w2', t2) <- checkWitnessM config kenv tenv w2
let w2TEC = reannotate fromAnT w2'
case t1 of
TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
| t11 `equivT` t2
-> returnX a
(\z -> XApp z x1' (XWitness w2TEC))
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 (TCon (TyConSpec TcConFun)) t11) t12
| t11 `equivT` t2
-> returnX a
(\z -> XApp z x1' x2')
t12
(effs1 `Sum.union` effs2)
(clos1 `Set.union` clos2)
TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) 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 UniverseSpec (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
| not $ configTrackedClosures config
= Just $ tBot kClosure
| otherwise
= trimClosure $ closureOfTaggedSet c2_cut
e2_captured
| not $ configTrackedEffects config
= tBot kEffect
| otherwise
= TSum e2
fun_result
| configFunctionalEffects config
, configFunctionalClosures config
= returnX a
(\z -> XLam z b1 x2')
(tFunEC t1 e2_captured c2_captured t2)
(Sum.empty kEffect)
c2_cut
| e2_captured == tBot kEffect
, c2_captured == tBot kClosure
= returnX a
(\z -> XLam z b1 x2')
(tFun t1 t2)
(Sum.empty kEffect)
Set.empty
| e2_captured /= tBot kEffect
= throw $ ErrorLamNotPure xx UniverseData e2_captured
| c2_captured /= tBot kClosure
= throw $ ErrorLamNotEmpty xx UniverseData c2_captured
| otherwise
= error "checkExpM': can't build function type."
in fun_result
Just UniverseWitness
| e2 /= Sum.empty kEffect
-> throw $ ErrorLamNotPure xx UniverseWitness (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
(w', tW) <- checkWitnessM config kenv tenv w
let wTEC = reannotate fromAnT 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 wTEC
returnX a
(\z -> XCast z c' x1')
t1 effs' clo
checkExpM' !config !kenv !tenv xx@(XCast a (CastForget w) x1)
= do
(w', tW) <- checkWitnessM config kenv tenv w
let wTEC = reannotate fromAnT 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 wTEC
returnX a
(\z -> XCast z c' x1')
t1 effs clos'
checkExpM' !config !kenv !tenv (XCast a CastSuspend x1)
= do
(x1', t1, effs, clos) <- checkExpM config kenv tenv x1
let tS = tApps (TCon (TyConSpec TcConSusp))
[TSum effs, t1]
returnX a
(\z -> XCast z CastSuspend x1')
tS (Sum.empty kEffect) clos
checkExpM' !config !kenv !tenv xx@(XCast a CastRun x1)
= do
(x1', t1, effs, clos) <- checkExpM config kenv tenv x1
case t1 of
TApp (TApp (TCon (TyConSpec TcConSusp)) eff2) tA
-> returnX a
(\z -> XCast z CastRun x1')
tA
(Sum.union effs (Sum.singleton kEffect eff2))
clos
_ -> throw $ ErrorRunNotSuspension xx t1
checkExpM' !_config !_kenv !_tenv xx@(XType _)
= throw $ ErrorNakedType xx
checkExpM' !_config !_kenv !_tenv xx@(XWitness _)
= throw $ ErrorNakedWitness xx
checkExpM' _ _ _ _
= error "checkExpM: can't check this expression"
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 (w', _) <- checkWitnessM config kenv tenv w
return ( XWitness (reannotate fromAnT 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 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'
return ( LLet 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)