Fix #11334.
authorRichard Eisenberg <eir@cis.upenn.edu>
Tue, 23 Feb 2016 02:47:32 +0000 (21:47 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Tue, 15 Mar 2016 01:44:17 +0000 (21:44 -0400)
Now we fail when trying to default non-*-kinded kind variables
with -XNoPolyKinds.

test case: dependent/should_fail/T11334

[skip ci]

compiler/typecheck/TcMType.hs
compiler/types/TyCoRep.hs
testsuite/tests/dependent/should_fail/T11334.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T11334.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T

index e8c120d..b905f53 100644 (file)
@@ -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
index 78adcd2..7ca9b26 100644 (file)
@@ -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 (file)
index 0000000..1f9970f
--- /dev/null
@@ -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 (file)
index 0000000..f7c87a3
--- /dev/null
@@ -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
index 08f6cf6..63f08d2 100644 (file)
@@ -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, [''])