[commit: ghc] wip/rae: Fix #11334. (208f43d)

[git at git.haskell.org]

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

On branch  : wip/rae
Link       : http://ghc.haskell.org/trac/ghc/changeset/208f43d58d7c5c0d4142407e4367353080f9f94b/ghc

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

commit 208f43d58d7c5c0d4142407e4367353080f9f94b
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Mon Feb 22 21:47:32 2016 -0500

    Fix #11334.
    
    Now we fail when trying to default non-*-kinded kind variables
    with -XNoPolyKinds.
    
    test case: dependent/should_fail/T11334


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

208f43d58d7c5c0d4142407e4367353080f9f94b
 compiler/typecheck/TcMType.hs                      | 36 ++++++++++++++++++++--
 compiler/types/TyCoRep.hs                          |  4 ++-
 testsuite/tests/dependent/should_fail/T11334.hs    |  8 +++++
 .../tests/dependent/should_fail/T11334.stderr      | 24 +++++++++++++++
 testsuite/tests/dependent/should_fail/all.T        |  1 +
 5 files changed, 69 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index e8c120d..b905f53 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -84,6 +84,7 @@ module TcMType (
 import TyCoRep
 import TcType
 import Type
+import Kind
 import Coercion
 import Class
 import Var
@@ -936,15 +937,23 @@ zonkQuantifiedTyVarOrType tv
              else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
 
--- | Take an (unconstrained) meta tyvar and default it. Works only for
--- kind vars (of type *) and RuntimeRep vars (of type RuntimeRep).
+-- | Take an (unconstrained) meta tyvar and default it. Works only on
+-- vars of type RuntimeRep and of type *. For other kinds, it issues
+-- an error. See Note [Defaulting with -XNoPolyKinds]
 defaultKindVar :: TcTyVar -> TcM Kind
 defaultKindVar kv
   | ASSERT( isMetaTyVar kv )
     isRuntimeRepVar kv
   = writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
-  | otherwise
+  | isStarKind (tyVarKind kv)
   = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
+  | otherwise
+  = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
+                      , text "of kind:" <+> ppr (tyVarKind kv')
+                      , text "Perhaps enable PolyKinds or add a kind signature" ])
+       ; return (mkTyVarTy kv) }
+  where
+    (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
@@ -970,6 +979,27 @@ skolemiseUnboundMetaTyVar tv details
         ; return final_tv }
 
 {-
+Note [Defaulting with -XNoPolyKinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data Compose f g a = Mk (f (g a))
+
+We infer
+
+  Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
+  Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
+        f (g a) -> Compose k1 k2 f g a
+
+Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
+What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
+we just defaulted all kind variables to *. But that's no good here,
+because the kind variables in 'Mk aren't of kind *, so defaulting to *
+is ill-kinded.
+
+After some debate on #11334, we decided to issue an error in this case.
+The code is in defaultKindVar.
+
 Note [What is a meta variable?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A "meta type-variable", also know as a "unification variable" is a placeholder
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 3798f69..c0a68d6 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -2882,7 +2882,9 @@ tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
 tidyOpenTyCoVar env@(_, subst) tyvar
   = case lookupVarEnv subst tyvar of
         Just tyvar' -> (env, tyvar')              -- Already substituted
-        Nothing     -> tidyTyCoVarBndr env tyvar  -- Treat it as a binder
+        Nothing     ->
+          let env' = tidyFreeTyCoVars env (tyCoVarsOfType (tyVarKind tyvar)) in
+          tidyTyCoVarBndr env' tyvar  -- Treat it as a binder
 
 ---------------
 tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
diff --git a/testsuite/tests/dependent/should_fail/T11334.hs b/testsuite/tests/dependent/should_fail/T11334.hs
new file mode 100644
index 0000000..1f9970f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T11334.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, NoPolyKinds #-}
+
+module T11334 where
+
+import Data.Functor.Compose
+import Data.Proxy
+
+p = Proxy :: Proxy 'Compose
diff --git a/testsuite/tests/dependent/should_fail/T11334.stderr b/testsuite/tests/dependent/should_fail/T11334.stderr
new file mode 100644
index 0000000..f7c87a3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T11334.stderr
@@ -0,0 +1,24 @@
+
+T11334.hs:8:14: error:
+    • Cannot default kind variable ‘f0’
+      of kind: k0 -> *
+      Perhaps enable PolyKinds or add a kind signature
+    • In an expression type signature: Proxy Compose
+      In the expression: Proxy :: Proxy Compose
+      In an equation for ‘p’: p = Proxy :: Proxy Compose
+
+T11334.hs:8:14: error:
+    • Cannot default kind variable ‘g0’
+      of kind: k10 -> k0
+      Perhaps enable PolyKinds or add a kind signature
+    • In an expression type signature: Proxy Compose
+      In the expression: Proxy :: Proxy Compose
+      In an equation for ‘p’: p = Proxy :: Proxy Compose
+
+T11334.hs:8:14: error:
+    • Cannot default kind variable ‘a0’
+      of kind: k10
+      Perhaps enable PolyKinds or add a kind signature
+    • In an expression type signature: Proxy Compose
+      In the expression: Proxy :: Proxy Compose
+      In an equation for ‘p’: p = Proxy :: Proxy Compose
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 08f6cf6..63f08d2 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -9,3 +9,4 @@ test('SelfDep', normal, compile_fail, [''])
 test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
+test('T11334', normal, compile_fail, [''])