Fix #14869 by being more mindful of Type vs. Constraint

Summary:
Before, we were using `isLiftedTypeKind` in `reifyType`
before checking if a type was `Constraint`. But as it turns out,
`isLiftedTypeKind` treats `Constraint` the same as `Type`, so every
occurrence of `Constraint` would be reified as `Type`! To make things
worse, the documentation for `isLiftedTypeKind` stated that it
treats `Constraint` //differently// from `Type`, which simply isn't
true.

This revises the documentation for `isLiftedTypeKind` to reflect
reality, and defers the `isLiftedTypeKind` check in `reifyType` so
that it does not accidentally swallow `Constraint`.

Test Plan: make test TEST=T14869

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14869

Differential Revision: https://phabricator.haskell.org/D4474

6 files changed, 99 insertions, 29 deletions

diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 00591d1bc2..30ad5095da 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1707,8 +1707,9 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
 ------------------------------
 reifyType :: TyCoRep.Type -> TcM TH.Type
 -- Monadic only because of failure
-reifyType ty                | isLiftedTypeKind ty = return TH.StarT
-                            | isConstraintKind ty = return TH.ConstraintT
+reifyType ty                | tcIsStarKind ty = return TH.StarT
+  -- Make sure to use tcIsStarKind here, since we don't want to confuse it
+  -- with Constraint (#14869).
 reifyType ty@(ForAllTy {})  = reify_for_all ty
 reifyType (LitTy t)         = do { r <- reifyTyLit t; return (TH.LitT r) }
 reifyType (TyVarTy tv)      = return (TH.VarT (reifyName tv))
@@ -1881,6 +1882,8 @@ reify_tc_app tc tys
          | isTupleTyCon tc                = if isPromotedDataCon tc
                                             then TH.PromotedTupleT arity
                                             else TH.TupleT arity
+         | tc `hasKey` constraintKindTyConKey
+                                          = TH.ConstraintT
          | tc `hasKey` funTyConKey        = TH.ArrowT
          | tc `hasKey` listTyConKey       = TH.ListT
          | tc `hasKey` nilDataConKey      = TH.PromotedNilT
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index 95a3bbf766..88ed114fe6 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -22,7 +22,7 @@ module Kind (
 
 import GhcPrelude
 
-import {-# SOURCE #-} Type    ( coreView, tcView
+import {-# SOURCE #-} Type    ( coreView
                               , splitTyConApp_maybe )
 import {-# SOURCE #-} DataCon ( DataCon )
 
@@ -128,25 +128,24 @@ isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
 -- like *, #, TYPE Lifted, TYPE v, Constraint.
 classifiesTypeWithValues :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
-classifiesTypeWithValues t | Just t' <- coreView t = classifiesTypeWithValues t'
-classifiesTypeWithValues (TyConApp tc [_]) = tc `hasKey` tYPETyConKey
-classifiesTypeWithValues _ = False
+classifiesTypeWithValues = isTYPE (const True)
 
--- | Is this kind equivalent to *?
+-- | Is this kind equivalent to @*@?
+--
+-- This considers 'Constraint' to be distinct from @*@. For a version that
+-- treats them as the same type, see 'isStarKind'.
 tcIsStarKind :: Kind -> Bool
-tcIsStarKind k | Just k' <- tcView k = isStarKind k'
-tcIsStarKind (TyConApp tc [TyConApp ptr_rep []])
-  =  tc      `hasKey` tYPETyConKey
-  && ptr_rep `hasKey` liftedRepDataConKey
-tcIsStarKind _ = False
+tcIsStarKind = tcIsTYPE is_lifted
+  where
+    is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
+    is_lifted _                        = False
 
--- | Is this kind equivalent to *?
+-- | Is this kind equivalent to @*@?
+--
+-- This considers 'Constraint' to be the same as @*@. For a version that
+-- treats them as different types, see 'tcIsStarKind'.
 isStarKind :: Kind -> Bool
-isStarKind k | Just k' <- coreView k = isStarKind k'
-isStarKind (TyConApp tc [TyConApp ptr_rep []])
-  =  tc      `hasKey` tYPETyConKey
-  && ptr_rep `hasKey` liftedRepDataConKey
-isStarKind _ = False
+isStarKind = isLiftedTypeKind
                               -- See Note [Kind Constraint and kind *]
 
 -- | Is the tycon @Constraint@?
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index cc425991ae..1082b5036d 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -39,6 +39,7 @@ module TyCoRep (
         mkTyConTy, mkTyVarTy, mkTyVarTys,
         mkFunTy, mkFunTys, mkForAllTy, mkForAllTys,
         mkPiTy, mkPiTys,
+        isTYPE, tcIsTYPE,
         isLiftedTypeKind, isUnliftedTypeKind,
         isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
         sameVis,
@@ -145,7 +146,7 @@ import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
                           , toposortTyVars
-                          , coreView )
+                          , coreView, tcView )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
 import {-# SOURCE #-} Coercion
@@ -706,22 +707,45 @@ mkTyConTy tycon = TyConApp tycon []
 Some basic functions, put here to break loops eg with the pretty printer
 -}
 
-is_TYPE :: (   Type    -- the single argument to TYPE; not a synonym
-            -> Bool )  -- what to return
-        -> Kind -> Bool
-is_TYPE f ki | Just ki' <- coreView ki = is_TYPE f ki'
-is_TYPE f (TyConApp tc [arg])
+-- | If a type is @'TYPE' r@ for some @r@, run the predicate argument on @r@.
+-- Otherwise, return 'False'.
+--
+-- This function does not distinguish between 'Constraint' and 'Type'. For a
+-- version which does distinguish between the two, see 'tcIsTYPE'.
+isTYPE :: (   Type    -- the single argument to TYPE; not a synonym
+           -> Bool )  -- what to return
+       -> Kind -> Bool
+isTYPE f ki | Just ki' <- coreView ki = isTYPE f ki'
+isTYPE f (TyConApp tc [arg])
   | tc `hasKey` tYPETyConKey
   = go arg
     where
       go ty | Just ty' <- coreView ty = go ty'
       go ty = f ty
-is_TYPE _ _ = False
+isTYPE _ _ = False
+
+-- | If a type is @'TYPE' r@ for some @r@, run the predicate argument on @r@.
+-- Otherwise, return 'False'.
+--
+-- This function distinguishes between 'Constraint' and 'Type' (and will return
+-- 'False' for 'Constraint'). For a version which does not distinguish between
+-- the two, see 'isTYPE'.
+tcIsTYPE :: (   Type    -- the single argument to TYPE; not a synonym
+             -> Bool )  -- what to return
+         -> Kind -> Bool
+tcIsTYPE f ki | Just ki' <- tcView ki = tcIsTYPE f ki'
+tcIsTYPE f (TyConApp tc [arg])
+  | tc `hasKey` tYPETyConKey
+  = go arg
+    where
+      go ty | Just ty' <- tcView ty = go ty'
+      go ty = f ty
+tcIsTYPE _ _ = False
 
--- | This version considers Constraint to be distinct from *. Returns True
--- if the argument is equivalent to Type and False otherwise.
+-- | This version considers Constraint to be the same as *. Returns True
+-- if the argument is equivalent to Type/Constraint and False otherwise.
 isLiftedTypeKind :: Kind -> Bool
-isLiftedTypeKind = is_TYPE is_lifted
+isLiftedTypeKind = isTYPE is_lifted
   where
     is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
     is_lifted _                        = False
@@ -730,7 +754,7 @@ isLiftedTypeKind = is_TYPE is_lifted
 -- Note that this returns False for levity-polymorphic kinds, which may
 -- be specialized to a kind that classifies unlifted types.
 isUnliftedTypeKind :: Kind -> Bool
-isUnliftedTypeKind = is_TYPE is_unlifted
+isUnliftedTypeKind = isTYPE is_unlifted
   where
     is_unlifted (TyConApp rr _args) = not (rr `hasKey` liftedRepDataConKey)
     is_unlifted _                   = False
diff --git a/testsuite/tests/th/T14869.hs b/testsuite/tests/th/T14869.hs
new file mode 100644
index 0000000000..c58d4e2720
--- /dev/null
+++ b/testsuite/tests/th/T14869.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14869 where
+
+import Data.Kind
+import GHC.Exts
+import Language.Haskell.TH (pprint, reify, stringE)
+
+type MyConstraint = Constraint
+type MyLiftedRep  = LiftedRep
+
+type family Foo1 :: Type
+type family Foo2 :: Constraint
+type family Foo3 :: MyConstraint
+type family Foo4 :: TYPE MyLiftedRep
+
+$(pure [])
+
+foo1, foo2, foo3 :: String
+foo1 = $(reify ''Foo1 >>= stringE . pprint)
+foo2 = $(reify ''Foo2 >>= stringE . pprint)
+foo3 = $(reify ''Foo3 >>= stringE . pprint)
+foo4 = $(reify ''Foo4 >>= stringE . pprint)
diff --git a/testsuite/tests/th/T14869.stderr b/testsuite/tests/th/T14869.stderr
new file mode 100644
index 0000000000..a2776b8cc8
--- /dev/null
+++ b/testsuite/tests/th/T14869.stderr
@@ -0,0 +1,17 @@
+T14869.hs:19:3-9: Splicing declarations pure [] ======>
+T14869.hs:22:10-42: Splicing expression
+    reify ''Foo1 >>= stringE . pprint
+  ======>
+    "type family T14869.Foo1 :: *"
+T14869.hs:23:10-42: Splicing expression
+    reify ''Foo2 >>= stringE . pprint
+  ======>
+    "type family T14869.Foo2 :: Constraint"
+T14869.hs:24:10-42: Splicing expression
+    reify ''Foo3 >>= stringE . pprint
+  ======>
+    "type family T14869.Foo3 :: T14869.MyConstraint"
+T14869.hs:25:10-42: Splicing expression
+    reify ''Foo4 >>= stringE . pprint
+  ======>
+    "type family T14869.Foo4 :: *"
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index b51059ca1c..f391012d2b 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -404,5 +404,7 @@ test('T14838', [], multimod_compile,
 test('T14817', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T14843', normal, compile, ['-v0'])
 test('T13776', normal, compile, ['-ddump-splices -v0'])
+test('T14869', normal, compile,
+    ['-v0 -ddump-splices -dsuppress-uniques ' + config.ghc_th_way_flags])
 test('T14888', normal, compile,
     ['-v0 -ddump-splices -dsuppress-uniques ' + config.ghc_th_way_flags])