[commit: ghc] master: Expand type synonyms when Linting a forall (9d600ea)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/9d600ea68c283b0d38ac663c3cc48baba6b94f57/ghc

>---------------------------------------------------------------

commit 9d600ea68c283b0d38ac663c3cc48baba6b94f57
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Jun 1 16:36:57 2018 +0100

    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.


>---------------------------------------------------------------

9d600ea68c283b0d38ac663c3cc48baba6b94f57
 compiler/coreSyn/CoreLint.hs        | 37 ++++++++++++++++++++++++++++++-------
 compiler/types/Type.hs              |  4 +++-
 testsuite/tests/polykinds/T14939.hs | 19 +++++++++++++++++++
 testsuite/tests/polykinds/all.T     |  1 +
 4 files changed, 53 insertions(+), 8 deletions(-)

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index d92082c..517b1be 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -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]
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 1e0ce99..9963208 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -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
index 0000000..eb3c700
--- /dev/null
+++ b/testsuite/tests/polykinds/T14939.hs
@@ -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
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 788832d..4fe88b2 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -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'])