diff options
Diffstat (limited to 'compiler/coreSyn/CoreLint.hs')
| -rw-r--r-- | compiler/coreSyn/CoreLint.hs | 107 |
1 files changed, 87 insertions, 20 deletions
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 349d36d8e2..21edba1241 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1352,9 +1352,10 @@ lintType ty@(FunTy t1 t2) ; k2 <- lintType t2 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 } -lintType t@(ForAllTy (TvBndr tv _vis) ty) - = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t) - ; lintTyBndr tv $ \tv' -> +lintType t@(ForAllTy (Bndr tv _vis) ty) + -- forall over types + | isTyVar tv + = do { lintTyBndr tv $ \tv' -> do { k <- lintType ty ; checkValueKind k (text "the body of forall:" <+> ppr t) ; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms] @@ -1364,6 +1365,20 @@ lintType t@(ForAllTy (TvBndr tv _vis) ty) , text "kind:" <+> ppr k ])) }} +lintType t@(ForAllTy (Bndr cv _vis) ty) + -- forall over coercions + = do { lintL (isCoVar cv) + (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t) + ; lintL (cv `elemVarSet` tyCoVarsOfType ty) + (text "Covar does not occur in the body:" <+> ppr t) + ; lintCoBndr cv $ \_ -> + do { k <- lintType ty + ; checkValueKind k (text "the body of forall:" <+> ppr t) + ; return liftedTypeKind + -- We don't check variable escape here. Namely, k could refer to cv' + -- See Note [NthCo and newtypes] in TyCoRep + }} + lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty) lintType (CastTy ty co) @@ -1491,11 +1506,11 @@ lint_app doc kfn kas addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka))) ; return kfb } - go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) tka@(ta,ka) - = do { let kv_kind = tyVarKind kv + go_app in_scope (ForAllTy (Bndr kv _vis) kfn) tka@(ta,ka) + = do { let kv_kind = varType kv ; unless (ka `eqType` kv_kind) $ addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka))) - ; return (substTyWithInScope in_scope [kv] [ta] kfn) } + ; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn } go_app _ kfn ka = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka))) @@ -1681,6 +1696,8 @@ lintCoercion co@(AppCo co1 co2) ---------- lintCoercion (ForAllCo tv1 kind_co co) + -- forall over types + | isTyVar tv1 = do { (_, k2) <- lintStarCoercion kind_co ; let tv2 = setTyVarKind tv1 k2 ; addInScopeVar tv1 $ @@ -1700,6 +1717,37 @@ lintCoercion (ForAllCo tv1 kind_co co) substTy subst t2 ; return (k3, k4, tyl, tyr, r) } } +lintCoercion (ForAllCo cv1 kind_co co) + -- forall over coercions + = ASSERT( isCoVar cv1 ) + do { (_, k2) <- lintStarCoercion kind_co + ; let cv2 = setVarType cv1 k2 + ; addInScopeVar cv1 $ + do { + ; (k3, k4, t1, t2, r) <- lintCoercion co + ; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co) + ; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co) + -- See Note [Weird typing rule for ForAllTy] in Type + ; in_scope <- getInScope + ; let tyl = mkTyCoInvForAllTy cv1 t1 + r2 = coVarRole cv1 + kind_co' = downgradeRole r2 Nominal kind_co + eta1 = mkNthCo r2 2 kind_co' + eta2 = mkNthCo r2 3 kind_co' + subst = mkCvSubst in_scope $ + -- We need both the free vars of the `t2` and the + -- free vars of the range of the substitution in + -- scope. All the free vars of `t2` and `kind_co` should + -- already be in `in_scope`, because they've been + -- linted and `cv2` has the same unique as `cv1`. + -- See Note [The substitution invariant] + unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2) + `mkTransCo` (mkSymCo eta2)) + tyr = mkTyCoInvForAllTy cv2 $ + substTy subst t2 + ; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } } + -- See Note [Weird typing rule for ForAllTy] in Type + lintCoercion co@(FunCo r co1 co2) = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2 @@ -1804,13 +1852,16 @@ lintCoercion co@(TransCo co1 co2) lintCoercion the_co@(NthCo r0 n co) = do { (_, _, s, t, r) <- lintCoercion co ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of - { (Just (tv_s, _ty_s), Just (tv_t, _ty_t)) - | n == 0 + { (Just (tcv_s, _ty_s), Just (tcv_t, _ty_t)) + -- works for both tyvar and covar + | n == 0 + , (isForAllTy_ty s && isForAllTy_ty t) + || (isForAllTy_co s && isForAllTy_co t) -> do { lintRole the_co Nominal r0 ; return (ks, kt, ts, tt, r0) } where - ts = tyVarKind tv_s - tt = tyVarKind tv_t + ts = varType tcv_s + tt = varType tcv_t ks = typeKind ts kt = typeKind tt @@ -1853,16 +1904,32 @@ lintCoercion (InstCo co arg) ; (k1',k2',s1,s2, r') <- lintCoercion arg ; lintRole arg Nominal r' ; in_scope <- getInScope - ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of - (Just (tv1,t1), Just (tv2,t2)) - | k1' `eqType` tyVarKind tv1 - , k2' `eqType` tyVarKind tv2 - -> return (k3, k4, - substTyWithInScope in_scope [tv1] [s1] t1, - substTyWithInScope in_scope [tv2] [s2] t2, r) - | otherwise - -> failWithL (text "Kind mis-match in inst coercion") - _ -> failWithL (text "Bad argument of inst") } + ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of + -- forall over tvar + { (Just (tv1,t1), Just (tv2,t2)) + | k1' `eqType` tyVarKind tv1 + , k2' `eqType` tyVarKind tv2 + -> return (k3, k4, + substTyWithInScope in_scope [tv1] [s1] t1, + substTyWithInScope in_scope [tv2] [s2] t2, r) + | otherwise + -> failWithL (text "Kind mis-match in inst coercion") + ; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of + -- forall over covar + { (Just (cv1, t1), Just (cv2, t2)) + | k1' `eqType` varType cv1 + , k2' `eqType` varType cv2 + , CoercionTy s1' <- s1 + , CoercionTy s2' <- s2 + -> do { return $ + (liftedTypeKind, liftedTypeKind + -- See Note [Weird typing rule for ForAllTy] in Type + , substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1 + , substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2 + , r) } + | otherwise + -> failWithL (text "Kind mis-match in inst coercion") + ; _ -> failWithL (text "Bad argument of inst") }}} lintCoercion co@(AxiomInstCo con ind cos) = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con)) |