Commit 9d600ea6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Expand type synonyms when Linting a forall

Trac #14939 showed a type like
   type Alg cls ob = ob
   f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b

where the kind of the forall looks like (Alg cls *), with a
free cls. This tripped up Core Lint.

I fixed this by making Core Lint a bit more forgiving, expanding
type synonyms if necessary.

I'm worried that this might not be the whole story; notably
typeKind looks suspect.  But it certainly fixes this problem.
parent 0e5d2b74
......@@ -1296,7 +1296,8 @@ lintInTy ty
= addLoc (InType ty) $
do { ty' <- applySubstTy ty
; k <- lintType ty'
; lintKind k
-- No need to lint k, because lintType
-- guarantees that k is linted
; return (ty', k) }
checkTyCon :: TyCon -> LintM ()
......@@ -1355,12 +1356,19 @@ lintType ty@(FunTy t1 t2)
lintType t@(ForAllTy (TvBndr tv _vis) ty)
= do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
; lintTyBndr tv $ \tv' ->
do { k <- lintType ty
; lintL (not (tv' `elemVarSet` tyCoVarsOfType k))
(text "Variable escape in forall:" <+> ppr t)
; lintL (classifiesTypeWithValues k)
(text "Non-* and non-# kind in forall:" <+> ppr t)
; return k }}
do { k <- lintType ty
; lintL (classifiesTypeWithValues k)
(text "Non-* and non-# kind in forall:" <+> ppr t)
; if (not (tv' `elemVarSet` tyCoVarsOfType k))
then return k
else
do { -- See Note [Stupid type synonyms]
let k' = expandTypeSynonyms k
; lintL (not (tv' `elemVarSet` tyCoVarsOfType k'))
(hang (text "Variable escape in forall:")
2 (vcat [ text "type:" <+> ppr t
, text "kind:" <+> ppr k' ]))
; return k' }}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
......@@ -1374,6 +1382,21 @@ lintType (CoercionTy co)
= do { (k1, k2, ty1, ty2, r) <- lintCoercion co
; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
{- Note [Stupid type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #14939)
type Alg cls ob = ob
f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b
Here 'cls' appears free in b's kind, which would usually be illegal
(becuase in (forall a. ty), ty's kind should not mention 'a'). But
#in this case (Alg cls *) = *, so all is well. Currently we allow
this, and make Lint expand synonyms where necessary to make it so.
c.f. TcUnify.occCheckExpand and CoreUtils.coreAltsType which deal
with the same problem. A single systematic solution eludes me.
-}
-----------------
lintTySynApp :: Bool -> Type -> TyCon -> [Type] -> LintM LintedKind
-- See Note [Linting type synonym applications]
......
......@@ -2311,10 +2311,12 @@ typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
typeKind (AppTy fun arg) = typeKind_apps fun [arg]
typeKind (LitTy l) = typeLiteralKind l
typeKind (FunTy {}) = liftedTypeKind
typeKind (ForAllTy _ ty) = typeKind ty
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (CastTy _ty co) = pSnd $ coercionKind co
typeKind (CoercionTy co) = coercionType co
typeKind (ForAllTy _ ty) = typeKind ty -- Urk. See Note [Stupid type synonyms]
-- in CoreLint. Maybe we should do
-- something similar here...
typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
-- The sole purpose of the function is to accumulate
......
{-# Language RankNTypes, ConstraintKinds, TypeInType, GADTs #-}
module T14939 where
import Data.Kind
type Cat ob = ob -> ob -> Type
type Alg cls ob = ob
newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where
Frí :: { with :: forall x. cls x => (a -> x) -> x }
-> Frí cls a
data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where
AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b
leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b)
leftAdj (AlgCat f) a = undefined
\ No newline at end of file
......@@ -192,3 +192,4 @@ test('SigTvKinds3', normal, compile_fail, [''])
test('T15116', normal, compile_fail, [''])
test('T15116a', normal, compile_fail, [''])
test('T15170', normal, compile, [''])
test('T14939', normal, compile, ['-O'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment