module DDC.Core.Check.Judge.Type.LamT (checkLamT) where import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum as Sum -- Check a spec abstraction. checkLamT :: Checker a n checkLamT !table !ctx mode _demand xx = case xx of XLAM a b1 x2 -> checkLAM table ctx a b1 x2 mode _ -> error "ddc-core.checkLamT: no match." -- When reconstructing the type of a type abstraction, -- the formal parameter must have a kind annotation: eg (/\v : K. x2) checkLAM !table !ctx0 a b1 x2 Recon = do let config = tableConfig table let xx = XLAM a b1 x2 -- Check the parameter ------------------ -- If the bound variable is named then it cannot shadow -- shadow others in the environment. when (memberKindBind b1 ctx0) $ throw $ ErrorLamShadow a xx b1 -- The parameter must have an explict kind annotation. let kA = typeOfBind b1 when (isHoleT config kA) $ throw $ ErrorLAMParamUnannotated a xx -- Check the kind annotation is well-sorted. (kA', sA, ctxA) <- checkTypeM config ctx0 UniverseKind kA Recon let b1' = replaceTypeOfBind kA' b1 -- The kind annotation must have sort Comp or Prop. when (not (sA == sComp) && not (sA == sProp)) $ throw $ ErrorLAMParamBadSort a xx b1 sA -- Check the body ----------------------- let (ctx2, pos1) = markContext ctxA let ctx3 = pushKind b1' RoleAbstract ctx2 let ctx4 = liftTypes 1 ctx3 -- Set the demand to 'None' because we don't want to force out -- suspensions. If the body of a type abstraction has any effects -- then this is a type error. (x2', t2, e2, ctx5) <- tableCheckExp table table ctx4 Recon DemandNone x2 -- Reconstruct the kind of the body. (t2', k2, ctx6) <- checkTypeM config ctx5 UniverseSpec t2 Recon -- The type of the body must have data kind. when (not $ isDataKind k2) $ throw $ ErrorLamBodyNotData a xx b1 t2' k2 -- The body of a spec abstraction must be pure. when (e2 /= Sum.empty kEffect) $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -- Cut the bound kind and elems under it from the context. let ctx_cut = lowerTypes 1 $ popToPos pos1 ctx6 -- Build the result type. let tResult = TForall b1' t2' ctrace $ vcat [ text "* LAM Recon" , indent 2 $ ppr (XLAM a b1' x2) , text " OUT: " <> ppr tResult , indent 2 $ ppr ctx0 , indent 2 $ ppr ctx_cut , empty ] returnX a (\z -> XLAM z b1' x2') tResult (Sum.empty kEffect) ctx_cut checkLAM !table !ctx0 a b1 x2 (Synth {}) = do let config = tableConfig table let xx = XLAM a b1 x2 -- Check the parameter ------------------ -- If the bound variable is named then it cannot shadow -- shadow others in the environment. when (memberKindBind b1 ctx0) $ throw $ ErrorLamShadow a xx b1 -- If the annotation is missing then make a new existential for it. let kA = typeOfBind b1 (kA', sA, ctxA) <- if isHoleT config kA then do iA <- newExists sComp let kA' = typeOfExists iA let ctxA = pushExists iA ctx0 return (kA', sComp, ctxA) else checkTypeM config ctx0 UniverseKind kA (Synth []) let b1' = replaceTypeOfBind kA' b1 -- The kind annotation must have sort Comp or Prop. when (not (sA == sComp) && not (sA == sProp)) $ throw $ ErrorLAMParamBadSort a xx b1 sA -- Check the body ----------------------- let (ctx2, pos1) = markContext ctxA let ctx3 = pushKind b1' RoleAbstract ctx2 let ctx4 = liftTypes 1 ctx3 -- Set the demand to 'None' because we don't want to force out -- suspensions. If the body of a type abstraction has any effects -- then this is a type error. (x2', t2, e2,ctx5) <- tableCheckExp table table ctx4 (Synth []) DemandNone x2 -- Force the kind of the body to be data. -- This is needed when the type of the body is an existential -- which doesn't yet have a resolved kind. t2' <- applyContext ctx5 t2 (_, _, ctx6) <- checkTypeM config ctx5 UniverseSpec t2' (Check kData) -- The body of a spec abstraction must be pure. when (e2 /= Sum.empty kEffect) $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -- Cut the bound kind and elems under it from the context. let ctx_cut = lowerTypes 1 $ popToPos pos1 ctx6 -- Build the result type. let tResult = TForall b1' t2 ctrace $ vcat [ text "* LAM Synth" , indent 2 $ ppr (XLAM a b1' x2) , text " OUT: " <> ppr tResult , indent 2 $ ppr ctx0 , indent 2 $ ppr ctx_cut , empty ] returnX a (\z -> XLAM z b1' x2') tResult (Sum.empty kEffect) ctx_cut checkLAM !table !ctx0 a b1 x2 (Check (TForall b tBody)) = do let config = tableConfig table let xx = XLAM a b1 x2 -- Check the parameter ------------------ -- If the bound variable is named then it cannot shadow -- shadow others in the environment. when (memberKindBind b1 ctx0) $ throw $ ErrorLamShadow a xx b1 -- If we have an expected kind for the parameter then it needs -- to be the same as any existing annotation. let kParam = typeOfBind b1 let kExpected = typeOfBind b -- If both the kind annotation is missing and there is no -- expected kind then we need to make an existential for it. (kA', sA, ctxA) <- if (isHoleT config kParam && isHoleT config kExpected) then do iA <- newExists sComp let kA' = typeOfExists iA let ctxA = pushExists iA ctx0 return (kA', sComp, ctxA) else if isHoleT config kExpected then do checkTypeM config ctx0 UniverseKind kParam (Synth []) else do checkTypeM config ctx0 UniverseKind kExpected (Synth []) let b1' = replaceTypeOfBind kA' b1 -- The kind annotation must have sort Comp or Prop. when (not (sA == sComp) && not (sA == sProp)) $ throw $ ErrorLAMParamBadSort a xx b1 sA -- Check the body ----------------------- let (ctx2, pos1) = markContext ctxA let ctx3 = pushKind b1' RoleAbstract ctx2 let ctx4 = liftTypes 1 ctx3 -- As the names used on the spec abstraction and quantifier are -- probably different, we use the binder name to instantiate -- the expected type. tBody_skol <- case takeSubstBoundOfBind b1 of Nothing -> return tBody Just u1 -> return $ substituteT b (TVar u1) tBody -- Set the demand to 'None' because we don't want to force out -- suspensions. If the body of a type abstraction has any effects -- then this is a type error. (x2', t2, e2, ctx5) <- tableCheckExp table table ctx4 (Check tBody_skol) DemandNone x2 -- Force the body of the spec abstraction must have data kind. -- This is needed when the type of the body is an existential -- which doesn't yet have a resolved kind. (t2', _k2, ctx6) <- checkTypeM config ctx5 UniverseSpec t2 (Check kData) -- The body of a spec abstraction must be pure. when (e2 /= Sum.empty kEffect) $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -- Apply context to synthesised type. -- We're about to pop the context back to how it was before the -- type lambda, and want to keep information gained from synthing -- the body. t2_sub <- applyContext ctx6 t2' -- Cut the bound kind and elems under it from the context. let ctx_cut = lowerTypes 1 $ popToPos pos1 ctx6 -- Build the result type. let tResult = TForall b1' t2_sub ctrace $ vcat [ text "* LAM" , indent 2 $ ppr (XLAM a b1' x2) , text " OUT: " <> ppr tResult , indent 2 $ ppr ctx0 , indent 2 $ ppr ctx_cut , empty ] returnX a (\z -> XLAM z b1' x2') tResult (Sum.empty kEffect) ctx_cut checkLAM table ctx0 a b1 x2 (Check tExpected) = checkSub table a ctx0 DemandNone (XLAM a b1 x2) tExpected