Expand type synonyms when Linting a forall
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 1 Jun 2018 15:36:57 +0000 (16:36 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 4 Jun 2018 09:35:34 +0000 (10:35 +0100)
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.

compiler/coreSyn/CoreLint.hs
compiler/types/Type.hs
testsuite/tests/polykinds/T14939.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index d92082c..517b1be 100644 (file)
@@ -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]
index 1e0ce99..9963208 100644 (file)
@@ -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
diff --git a/testsuite/tests/polykinds/T14939.hs b/testsuite/tests/polykinds/T14939.hs
new file mode 100644 (file)
index 0000000..eb3c700
--- /dev/null
@@ -0,0 +1,19 @@
+{-# 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
index 788832d..4fe88b2 100644 (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'])