Build only well-kinded types in type checker
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 11 Dec 2017 11:52:44 +0000 (11:52 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 11 Dec 2017 15:30:10 +0000 (15:30 +0000)
During type inference, we maintain the invariant that every type is
well-kinded /without/ zonking; and in particular that typeKind does
not fail (as it can for ill-kinded types).

But TcHsType.tcInferApps was not guaranteeing this invariant,
resulting in Trac #14174 and #14520.

This patch fixes it, making things better -- but it does /not/
fix the program in Trac #14174 comment:5, which still crashes.
So more work to be done.

See Note [Ensure well-kinded types] in TcHsType

compiler/typecheck/TcHsType.hs
testsuite/tests/polykinds/T14174.hs [new file with mode: 0644]
testsuite/tests/polykinds/T14174.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T14174a.hs [new file with mode: 0644]
testsuite/tests/polykinds/T14174a.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T14520.hs [new file with mode: 0644]
testsuite/tests/polykinds/T14520.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index 7807ab1..72bc843 100644 (file)
@@ -64,6 +64,7 @@ import TcSimplify ( solveEqualities )
 import TcType
 import TcHsSyn( zonkSigType )
 import Inst   ( tcInstBinders, tcInstBinder )
+import TyCoRep( Type( CastTy ) )
 import Type
 import Kind
 import RdrName( lookupLocalRdrOcc )
@@ -869,16 +870,40 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
       | otherwise
          -- Even after substituting, still no binders. Use matchExpectedFunKind
       = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
-           ; (co, arg_k, res_k)
-               <- matchExpectedFunKind (mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args))
-                                       substed_inner_ki
-           ; let subst' = zapped_subst `extendTCvInScopeSet` tyCoVarsOfTypes [arg_k, res_k]
-           ; go n acc_args subst' (fun `mkNakedCastTy` co)
-                [mkAnonBinder arg_k] res_k all_args }
+           ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
+           ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
+                 subst'       = zapped_subst `extendTCvInScopeSet` new_in_scope
+           ; go n acc_args subst'
+                (fun `CastTy` co)      -- NB: CastTy, not mkCastTy or mkNakedCastTy!
+                                       -- See Note [Ensure well-kinded types]
+                [mkAnonBinder arg_k]
+                res_k all_args }
       where
         substed_inner_ki               = substTy subst inner_ki
         (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
         zapped_subst                   = zapTCvSubst subst
+        hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
+
+{- Note [Ensure well-kinded types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During type inference, we maintain the invariant that every type is
+well-kinded /without/ zonking; and in particular that typeKind does not
+fail (as it can for ill-kinded types).
+
+We need to be careful at this point. Suppose we are kind-checking the
+type (a Int), where (a :: kappa). Then in tcInferApps we'll run out of
+binders on a's kind, so we'll call matchExpectedFunKind, and unify
+   kappa := kappa1 -> kappa2,  with evidence co :: kappa ~ (kappa1 ~ kappa2)
+But that evidence is actually Refl, so if we use the smart constructor
+mkNakedCastTy, we'll form the result type
+   ((a::kappa) (Int::*))
+which does not satisfy the invariant, and crashes TypeKind.  This
+caused Trac #14174 and #14520.
+
+Solution: use an actual CastTy. Now everything is well-kinded.
+The CastTy will be removed later, when we zonk.  Still, it's
+distressingly delicate.
+-}
 
 -- | Applies a type to a list of arguments.
 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
@@ -1873,6 +1898,9 @@ tcTyClTyVars tycon_name thing_inside
              res_kind   = tyConResKind tycon
              binders    = correct_binders (tyConBinders tycon) res_kind
 
+       ; traceTc "tcTyClTyVars" (vcat [ ppr tycon
+                                      , ppr (tyConBinders tycon)
+                                      , ppr (tcTyConScopedTyVars tycon) ])
           -- See Note [Free-floating kind vars]
        ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
        ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
diff --git a/testsuite/tests/polykinds/T14174.hs b/testsuite/tests/polykinds/T14174.hs
new file mode 100644 (file)
index 0000000..7a58b70
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE  TypeInType, RankNTypes, KindSignatures, PolyKinds #-}
+module T14174 where
+
+data T k (x :: k) = MkT
+
+data S x = MkS (T (x Int) x)
diff --git a/testsuite/tests/polykinds/T14174.stderr b/testsuite/tests/polykinds/T14174.stderr
new file mode 100644 (file)
index 0000000..4aafa64
--- /dev/null
@@ -0,0 +1,7 @@
+
+T14174.hs:6:27: error:
+    • Expecting one more argument to ‘x’
+      Expected kind ‘x Int’, but ‘x’ has kind ‘* -> *’
+    • In the second argument of ‘T’, namely ‘x’
+      In the type ‘(T (x Int) x)’
+      In the definition of data constructor ‘MkS’
diff --git a/testsuite/tests/polykinds/T14174a.hs b/testsuite/tests/polykinds/T14174a.hs
new file mode 100644 (file)
index 0000000..82f418b
--- /dev/null
@@ -0,0 +1,56 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14174a where
+
+import Data.Kind
+
+data TyFun :: * -> * -> *
+type a ~> b = TyFun a b -> *
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) | (:~>)
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+type family ElimBool (p :: Bool -> Type)
+                     (z :: Bool)
+                     (pFalse :: p False)
+                     (pTrue  :: p True)
+            :: p z where
+  -- Commenting out the line below makes the panic go away
+  ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue
+
+type family ElimBoolPoly (arr :: FunArrow)
+                         (p :: (Bool -?> Type) arr)
+                         (z :: Bool)
+                         (pFalse :: App Bool arr Type p False)
+                         (pTrue  :: App Bool arr Type p True)
+            :: App Bool arr Type p z
diff --git a/testsuite/tests/polykinds/T14174a.stderr b/testsuite/tests/polykinds/T14174a.stderr
new file mode 100644 (file)
index 0000000..139597f
--- /dev/null
@@ -0,0 +1,2 @@
+
+
diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs
new file mode 100644 (file)
index 0000000..ed87035
--- /dev/null
@@ -0,0 +1,16 @@
+{-# Language TypeInType, TypeFamilies, TypeOperators #-}
+
+module T14520 where
+
+import Data.Kind
+
+type a ~>> b = (a, b) -> Type
+
+data family Sing (a::k)
+
+type family XXX (f::a~>>b) (x::a) :: b
+
+type family Id   :: (kat :: a ~>> (a ~>> *)) `XXX` (b :: a) `XXX` b
+
+sId :: Sing w -> Sing (Id :: bat w w)
+sId = sId
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
new file mode 100644 (file)
index 0000000..e19d834
--- /dev/null
@@ -0,0 +1,5 @@
+
+T14520.hs:15:24: error:
+    • Expected kind ‘bat w w’, but ‘Id’ has kind ‘XXX (XXX kat0 b0) b0’
+    • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
+      In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
index 73408e8..9f34f30 100644 (file)
@@ -174,3 +174,6 @@ test('T13391', normal, compile_fail, [''])
 test('T13391a', normal, compile, [''])
 test('T14270', normal, compile, [''])
 test('T14450', normal, compile_fail, [''])
+test('T14174', normal, compile_fail, [''])
+test('T14174a', expect_broken(14174), compile_fail, [''])
+test('T14520', normal, compile_fail, [''])