Treat isConstraintKind more consistently
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 25 Jul 2018 10:35:43 +0000 (11:35 +0100)
committerBen Gamari <ben@smart-cactus.org>
Thu, 2 Aug 2018 02:42:22 +0000 (22:42 -0400)
It turned out that we were not being consistent
about our use of isConstraintKind.

It's delicate, because the typechecker treats Constraint and Type as
/distinct/, whereas they are the /same/ in the rest of the compiler
(Trac #11715).

And had it wrong, which led to Trac #15412.  This patch does the
following:

* Rename isConstraintKind      to tcIsConstraintKind
         returnsConstraintKind to tcReturnsConstraintKind
  to emphasise that they use the 'tcView' view of types.

* Move these functions, and some related ones (tcIsLiftedTypeKind),
  from Kind.hs, to group together in Type.hs, alongside isPredTy.

It feels very unsatisfactory that these 'tcX' functions live in Type,
but it happens because isPredTy is called later in the compiler
too.  But it's a consequence of the 'Constraint vs Type' dilemma.

(cherry picked from commit c5d31df70b16dc346b5860077c8bbe585ddb7a78)

16 files changed:
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
compiler/types/Kind.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs
compiler/types/Unify.hs
testsuite/tests/rename/should_fail/T5513.stderr
testsuite/tests/typecheck/should_compile/T15412.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 9a45d7a..355a9e3 100644 (file)
@@ -20,7 +20,6 @@ import TcType
 import RnUnbound ( unknownNameSuggestions )
 import Type
 import TyCoRep
-import Kind
 import Unify            ( tcMatchTys )
 import Module
 import FamInst
@@ -1933,8 +1932,7 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
   | KindLevel <- level, occurs_check_error       = (True, Nothing, empty)
   | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
   | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
-  | isLiftedTypeKind exp && not (isConstraintKind exp)
-                                                 = (False, Nothing, msg4)
+  | tcIsLiftedTypeKind exp                       = (False, Nothing, msg4)
   | Just msg <- num_args_msg                     = (False, Nothing, msg $$ msg1)
   | KindLevel <- level, Just th <- maybe_thing   = (False, Nothing, msg5 th)
   | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
@@ -1989,7 +1987,7 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
                  2 (text "but" <+> quotes th <+> text "has kind" <+>
                     quotes (ppr act))
       where
-        kind_desc | isConstraintKind exp = text "a constraint"
+        kind_desc | tcIsConstraintKind exp = text "a constraint"
 
                     -- TYPE t0
                   | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp
index 4480af1..a9e48a6 100644 (file)
@@ -74,7 +74,6 @@ import Inst   ( tcInstTyBinders, tcInstTyBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
 import Coercion
-import Kind
 import RdrName( lookupLocalRdrOcc )
 import Var
 import VarSet
@@ -696,7 +695,7 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
   = do { ctxt' <- tc_hs_context mode ctxt
 
          -- See Note [Body kind of a HsQualTy]
-       ; ty' <- if isConstraintKind exp_kind
+       ; ty' <- if tcIsConstraintKind exp_kind
                 then tc_lhs_type mode ty constraintKind
                 else do { ek <- newOpenTypeKind
                                 -- The body kind (result of the function)
@@ -842,9 +841,9 @@ tupKindSort_maybe :: TcKind -> Maybe TupleSort
 tupKindSort_maybe k
   | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
   | Just k'      <- tcView k            = tupKindSort_maybe k'
-  | isConstraintKind k = Just ConstraintTuple
-  | isLiftedTypeKind k = Just BoxedTuple
-  | otherwise          = Nothing
+  | tcIsConstraintKind k = Just ConstraintTuple
+  | tcIsLiftedTypeKind k   = Just BoxedTuple
+  | otherwise            = Nothing
 
 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
 tc_tuple rn_ty mode tup_sort tys exp_kind
index e8ca707..59a90d5 100644 (file)
@@ -42,7 +42,6 @@ import TcUnify
 import CoreSyn    ( Expr(..), mkApps, mkVarApps, mkLams )
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import CoreUnfold ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
-import Kind
 import Type
 import TcEvidence
 import TyCon
index 2ad93b0..92089af 100644 (file)
@@ -16,7 +16,6 @@ import TcFlatten
 import TcUnify( canSolveByUnification )
 import VarSet
 import Type
-import Kind( isConstraintKind )
 import InstEnv( DFunInstType, lookupInstEnv
               , instanceDFunId, isOverlappable )
 import CoAxiom( sfInteractTop, sfInteractInert )
@@ -2811,7 +2810,7 @@ matchTypeable clas [k,t]  -- clas = Typeable
   -- Now cases that do work
   | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
   | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
-  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
+  | tcIsConstraintKind t                   = doTyConApp clas t constraintKindTyCon []
   | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
   , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
index 11c9083..3f3252f 100644 (file)
@@ -98,7 +98,6 @@ import GhcPrelude
 import TyCoRep
 import TcType
 import Type
-import Kind
 import Coercion
 import Class
 import Var
@@ -723,9 +722,9 @@ writeMetaTyVarRef tyvar ref ty
        ; zonked_ty      <- zonkTcType ty
        ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
                                                   -- otherwise, we can panic in piResultTy
-             kind_check_ok = isConstraintKind zonked_tv_kind
+             kind_check_ok = tcIsConstraintKind zonked_tv_kind
                           || tcEqKind zonked_ty_kind zonked_tv_kind
-             -- Hack alert! isConstraintKind: see TcHsType
+             -- Hack alert! tcIsConstraintKind: see TcHsType
              -- Note [Extra-constraint holes in partial type signatures]
 
              kind_msg = hang (text "Ill-kinded update to meta tyvar")
index 34bf73e..31695e3 100644 (file)
@@ -69,7 +69,6 @@ import RnTypes
 import TcHsSyn
 import TcSimplify
 import Type
-import Kind
 import NameSet
 import TcMType
 import TcHsType
index 0dc88f2..7367326 100644 (file)
@@ -47,7 +47,6 @@ import FamInstEnv
 import Coercion
 import Type
 import TyCoRep   -- for checkValidRoles
-import Kind
 import Class
 import CoAxiom
 import TyCon
@@ -993,7 +992,8 @@ tcTyClDecl1 _parent roles_info
     do { clas <- fixM $ \ clas ->
             -- We need the knot because 'clas' is passed into tcClassATs
             tcTyClTyVars class_name $ \ binders res_kind ->
-            do { MASSERT( isConstraintKind res_kind )
+            do { MASSERT2( tcIsConstraintKind res_kind
+                         , ppr class_name $$ ppr res_kind )
                ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
                ; let tycon_name = class_name        -- We use the same name
                      roles = roles_info tycon_name  -- for TyCon and Class
index fccb105..eca7c01 100644 (file)
@@ -2141,6 +2141,40 @@ isImprovementPred ty
       IrredPred {}       -> True -- Might have equalities after reduction?
       ForAllPred {}      -> False
 
+-- | Is the equality
+--        a ~r ...a....
+-- definitely insoluble or not?
+--      a ~r Maybe a      -- Definitely insoluble
+--      a ~N ...(F a)...  -- Not definitely insoluble
+--                        -- Perhaps (F a) reduces to Int
+--      a ~R ...(N a)...  -- Not definitely insoluble
+--                        -- Perhaps newtype N a = MkN Int
+-- See Note [Occurs check error] in
+-- TcCanonical for the motivation for this function.
+isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
+isInsolubleOccursCheck eq_rel tv ty
+  = go ty
+  where
+    go ty | Just ty' <- tcView ty = go ty'
+    go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
+    go (LitTy {})    = False
+    go (AppTy t1 t2) = case eq_rel of  -- See Note [AppTy and ReprEq]
+                         NomEq  -> go t1 || go t2
+                         ReprEq -> go t1
+    go (FunTy t1 t2) = go t1 || go t2
+    go (ForAllTy (TvBndr tv' _) inner_ty)
+      | tv' == tv = False
+      | otherwise = go (tyVarKind tv') || go inner_ty
+    go (CastTy ty _)  = go ty   -- ToDo: what about the coercion
+    go (CoercionTy _) = False   -- ToDo: what about the coercion
+    go (TyConApp tc tys)
+      | isGenerativeTyCon tc role = any go tys
+      | otherwise                 = any go (drop (tyConArity tc) tys)
+         -- (a ~ F b a), where F has arity 1,
+         -- has an insoluble occurs check
+
+    role = eqRelRole eq_rel
+
 {- Note [Expanding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we expand superclasses, we use the following algorithm:
@@ -2212,7 +2246,7 @@ the quantified variables.
 
 ************************************************************************
 *                                                                      *
-\subsection{Predicates}
+      Classifying types
 *                                                                      *
 ************************************************************************
 -}
@@ -2314,39 +2348,6 @@ isTyVarHead _  (ForAllTy {})   = False
 isTyVarHead _  (FunTy {})      = False
 isTyVarHead _  (CoercionTy {}) = False
 
--- | Is the equality
---        a ~r ...a....
--- definitely insoluble or not?
---      a ~r Maybe a      -- Definitely insoluble
---      a ~N ...(F a)...  -- Not definitely insoluble
---                        -- Perhaps (F a) reduces to Int
---      a ~R ...(N a)...  -- Not definitely insoluble
---                        -- Perhaps newtype N a = MkN Int
--- See Note [Occurs check error] in
--- TcCanonical for the motivation for this function.
-isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
-isInsolubleOccursCheck eq_rel tv ty
-  = go ty
-  where
-    go ty | Just ty' <- tcView ty = go ty'
-    go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
-    go (LitTy {})    = False
-    go (AppTy t1 t2) = case eq_rel of  -- See Note [AppTy and ReprEq]
-                         NomEq  -> go t1 || go t2
-                         ReprEq -> go t1
-    go (FunTy t1 t2) = go t1 || go t2
-    go (ForAllTy (TvBndr tv' _) inner_ty)
-      | tv' == tv = False
-      | otherwise = go (tyVarKind tv') || go inner_ty
-    go (CastTy ty _)  = go ty   -- ToDo: what about the coercion
-    go (CoercionTy _) = False   -- ToDo: what about the coercion
-    go (TyConApp tc tys)
-      | isGenerativeTyCon tc role = any go tys
-      | otherwise                 = any go (drop (tyConArity tc) tys)
-         -- (a ~ F b a), where F has arity 1,
-         -- has an insoluble occurs check
-
-    role = eqRelRole eq_rel
 
 {- Note [AppTy and ReprEq]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
index 0dc5664..7c6db0e 100644 (file)
@@ -32,7 +32,6 @@ import TcType hiding ( sizeType, sizeTypes )
 import PrelNames
 import Type
 import Coercion
-import Kind
 import CoAxiom
 import Class
 import TyCon
@@ -384,10 +383,10 @@ checkValidMonoType ty
 
 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
 checkTySynRhs ctxt ty
-  | returnsConstraintKind actual_kind
+  | tcReturnsConstraintKind actual_kind
   = do { ck <- xoptM LangExt.ConstraintKinds
        ; if ck
-         then  when (isConstraintKind actual_kind)
+         then  when (tcIsConstraintKind actual_kind)
                     (do { dflags <- getDynFlags
                         ; check_pred_ty emptyTidyEnv dflags ctxt ty })
          else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
@@ -1317,7 +1316,8 @@ checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
                    -> TcM ([TyVar], ThetaType, Class, [Type])
 checkValidInstance ctxt hs_type ty
   | not is_tc_app
-  = failWithTc (text "Instance head is not headed by a class")
+  = failWithTc (hang (text "Instance head is not headed by a class:")
+                   2 ( ppr tau))
 
   | isNothing mb_cls
   = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
index 0ce6bfe..f88bbe1 100644 (file)
@@ -7,13 +7,10 @@ module Kind (
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind,
-        isConstraintKind,
         isTYPEApp,
-        returnsTyCon, returnsConstraintKind,
         isConstraintKindCon,
 
         classifiesTypeWithValues,
-        tcIsLiftedTypeKind,
         isKindLevPoly
        ) where
 
@@ -64,13 +61,8 @@ distinct uniques, they are treated as equal at all times except
 during type inference.
 -}
 
-isConstraintKind :: Kind -> Bool
 isConstraintKindCon :: TyCon -> Bool
-
-isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
-
-isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
-isConstraintKind _               = False
+isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
 
 isTYPEApp :: Kind -> Maybe DataCon
 isTYPEApp (TyConApp tc args)
@@ -81,17 +73,6 @@ isTYPEApp (TyConApp tc args)
   = Just dc
 isTYPEApp _ = Nothing
 
--- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
--- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
-returnsTyCon :: Unique -> Type -> Bool
-returnsTyCon tc_u (ForAllTy _ ty)  = returnsTyCon tc_u ty
-returnsTyCon tc_u (FunTy    _ ty)  = returnsTyCon tc_u ty
-returnsTyCon tc_u (TyConApp tc' _) = tc' `hasKey` tc_u
-returnsTyCon _  _                  = False
-
-returnsConstraintKind :: Kind -> Bool
-returnsConstraintKind = returnsTyCon constraintKindTyConKey
-
 -- | Tests whether the given kind (which should look like @TYPE x@)
 -- is something other than a constructor tree (that is, constructors at every node).
 -- E.g.  True of   TYPE k, TYPE (F Int)
@@ -130,13 +111,3 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
 classifiesTypeWithValues :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
 classifiesTypeWithValues = isTYPE (const True)
-
--- | Is this kind equivalent to @*@?
---
--- This considers 'Constraint' to be distinct from @*@. For a version that
--- treats them as the same type, see 'isLiftedTypeKind'.
-tcIsLiftedTypeKind :: Kind -> Bool
-tcIsLiftedTypeKind = tcIsTYPE is_lifted
-  where
-    is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
-    is_lifted _                        = False
index 417495b..e6bc7e0 100644 (file)
@@ -41,7 +41,7 @@ module TyCoRep (
         mkTyConTy, mkTyVarTy, mkTyVarTys,
         mkFunTy, mkFunTys, mkForAllTy, mkForAllTys,
         mkPiTy, mkPiTys,
-        isTYPE, tcIsTYPE,
+        isTYPE,
         isLiftedTypeKind, isUnliftedTypeKind,
         isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
         sameVis,
@@ -148,7 +148,7 @@ import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
                           , toposortTyVars
-                          , coreView, tcView )
+                          , coreView )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
 import {-# SOURCE #-} Coercion
@@ -798,24 +798,6 @@ isTYPE f (TyConApp tc [arg])
       go ty = f ty
 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 the same as *. Returns True
 -- if the argument is equivalent to Type/Constraint and False otherwise.
 -- See Note [Kind Constraint and kind Type]
index e8b79db..5c6ea9b 100644 (file)
@@ -121,6 +121,7 @@ module Type (
 
         -- ** Finding the kind of a type
         typeKind, isTypeLevPoly, resultIsLevPoly,
+        tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
 
         -- ** Common Kind
         liftedTypeKind,
@@ -229,7 +230,13 @@ import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
                                  , typeSymbolKind, liftedTypeKind )
 import PrelNames
 import CoAxiom
-import {-# SOURCE #-} Coercion
+import {-# SOURCE #-} Coercion( mkCoherenceCo, mkReflCo
+                              , mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
+                              , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
+                              , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
+                              , mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo
+                              , decomposePiCos, coercionKind, coercionType
+                              , isReflexiveCo, seqCo )
 
 -- others
 import Util
@@ -322,34 +329,10 @@ See also Trac #11715, which tracks removing this inconsistency.
 
 -}
 
-{-# INLINE coreView #-}
-coreView :: Type -> Maybe Type
--- ^ This function Strips off the /top layer only/ of a type synonym
--- application (if any) its underlying representation type.
--- Returns Nothing if there is nothing to look through.
--- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
---
--- By being non-recursive and inlined, this case analysis gets efficiently
--- joined onto the case analysis that the caller is already doing
-coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
-  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
-               -- The free vars of 'rhs' should all be bound by 'tenv', so it's
-               -- ok to use 'substTy' here.
-               -- See also Note [The substitution invariant] in TyCoRep.
-               -- Its important to use mkAppTys, rather than (foldl AppTy),
-               -- because the function part might well return a
-               -- partially-applied type constructor; indeed, usually will!
-
-coreView (TyConApp tc [])       -- At the Core level, Constraint = Type
-  | isConstraintKindCon tc
-  = Just liftedTypeKind
-
-coreView _ = Nothing
-
 -- | Gives the typechecker view of a type. This unwraps synonyms but
 -- leaves 'Constraint' alone. c.f. coreView, which turns Constraint into
 -- TYPE LiftedRep. Returns Nothing if no unwrapping happens.
--- See also Note [coreView vs tcView] in Type.
+-- See also Note [coreView vs tcView]
 {-# INLINE tcView #-}
 tcView :: Type -> Maybe Type
 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
@@ -362,6 +345,28 @@ tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
                -- partially-applied type constructor; indeed, usually will!
 tcView _ = Nothing
 
+{-# INLINE coreView #-}
+coreView :: Type -> Maybe Type
+-- ^ This function Strips off the /top layer only/ of a type synonym
+-- application (if any) its underlying representation type.
+-- Returns Nothing if there is nothing to look through.
+-- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
+--
+-- By being non-recursive and inlined, this case analysis gets efficiently
+-- joined onto the case analysis that the caller is already doing
+coreView ty@(TyConApp tc tys)
+  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
+  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
+    -- This equation is exactly like tcView
+
+  -- At the Core level, Constraint = Type
+  -- See Note [coreView vs tcView]
+  | isConstraintKindCon tc
+  = ASSERT2( null tys, ppr ty )
+    Just liftedTypeKind
+
+coreView _ = Nothing
+
 -----------------------------------------------
 expandTypeSynonyms :: Type -> Type
 -- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
@@ -731,14 +736,14 @@ repSplitAppTy_maybe (TyConApp tc tys)
 
 repSplitAppTy_maybe _other = Nothing
 
--- this one doesn't braek apart (c => t).
+-- This one doesn't break apart (c => t).
 -- See Note [Decomposing fat arrow c=>t]
 -- Defined here to avoid module loops between Unify and TcType.
 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
 -- any coreView stuff is already done. Refuses to look through (c => t)
 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
-  | isConstraintKind (typeKind ty1)
+  | isPredTy ty1
   = Nothing  -- See Note [Decomposing fat arrow c=>t]
 
   | otherwise
@@ -754,18 +759,6 @@ tcRepSplitAppTy_maybe (TyConApp tc tys)
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 tcRepSplitAppTy_maybe _other = Nothing
 
--- | Split a type constructor application into its type constructor and
--- applied types. Note that this may fail in the case of a 'FunTy' with an
--- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
--- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
--- type before using this function.
---
--- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
-tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
--- Defined here to avoid module loops between Unify and TcType.
-tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
-tcSplitTyConApp_maybe ty                         = tcRepSplitTyConApp_maybe ty
-
 -- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
 tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 -- Defined here to avoid module loops between Unify and TcType.
@@ -1562,6 +1555,56 @@ But there are a number of complications:
   want to print it nicely in error messages.
 -}
 
+-- | Split a type constructor application into its type constructor and
+-- applied types. Note that this may fail in the case of a 'FunTy' with an
+-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
+-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
+-- type before using this function.
+--
+-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
+tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+-- Defined here to avoid module loops between Unify and TcType.
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
+tcSplitTyConApp_maybe ty                         = tcRepSplitTyConApp_maybe ty
+
+-- tcIsConstraintKind stuf only makes sense in the typechecker
+-- After that Constraint = Type
+-- See Note [coreView vs tcView]
+-- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh)
+tcIsConstraintKind :: Kind -> Bool
+tcIsConstraintKind ty
+  | Just (tc, args) <- tcSplitTyConApp_maybe ty    -- Note: tcSplit here
+  , isConstraintKindCon tc
+  = ASSERT2( null args, ppr ty ) True
+
+  | otherwise
+  = False
+
+-- | Is this kind equivalent to @*@?
+--
+-- This considers 'Constraint' to be distinct from @*@. For a version that
+-- treats them as the same type, see 'isLiftedTypeKind'.
+tcIsLiftedTypeKind :: Kind -> Bool
+tcIsLiftedTypeKind ty
+  | Just (type_tc, [arg]) <- tcSplitTyConApp_maybe ty
+  , type_tc `hasKey` tYPETyConKey
+  , Just (lifted_rep_tc, args) <- tcSplitTyConApp_maybe arg
+  , lifted_rep_tc `hasKey` liftedRepDataConKey
+  = ASSERT2( null args, ppr ty ) True
+  | otherwise
+  = False
+
+tcReturnsConstraintKind :: Kind -> Bool
+-- True <=> the Kind ultimately returns a Constraint
+--   E.g.  * -> Constraint
+--         forall k. k -> Constraint
+tcReturnsConstraintKind kind
+  | Just kind' <- tcView kind = tcReturnsConstraintKind kind'
+tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty
+tcReturnsConstraintKind (FunTy    _ ty) = tcReturnsConstraintKind ty
+tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
+tcReturnsConstraintKind _               = False
+
 -- | Is the type suitable to classify a given/wanted in the typechecker?
 isPredTy :: Type -> Bool
 -- See Note [isPredTy complications]
@@ -1589,7 +1632,7 @@ isPredTy ty = go ty []
 
     go_k :: Kind -> [KindOrType] -> Bool
     -- True <=> ('k' applied to 'kts') = Constraint
-    go_k k [] = isConstraintKind k
+    go_k k [] = tcIsConstraintKind k
     go_k k (arg:args) = case piResultTy_maybe k arg of
                           Just k' -> go_k k' args
                           Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
index edd82ba..581cbb3 100644 (file)
@@ -31,7 +31,6 @@ import GhcPrelude
 import Var
 import VarEnv
 import VarSet
-import Kind
 import Name( Name )
 import Type hiding ( getTvSubstEnv )
 import Coercion hiding ( getCvSubstEnv )
index 7e26622..4ce02ac 100644 (file)
@@ -1,4 +1,4 @@
 
 T5513.hs:4:19: error:
-    • Instance head is not headed by a class
+    • Instance head is not headed by a class: lowercase_name a
     • In the stand-alone deriving instance for ‘lowercase_name a’
diff --git a/testsuite/tests/typecheck/should_compile/T15412.hs b/testsuite/tests/typecheck/should_compile/T15412.hs
new file mode 100644 (file)
index 0000000..6458ae0
--- /dev/null
@@ -0,0 +1,17 @@
+{-# Language DataKinds, TypeInType, TypeFamilies, UndecidableInstances #-}
+
+module T15412 where
+
+import Data.Kind
+
+newtype I a = I a
+
+type C = Constraint
+
+type family
+  UnitC :: C where
+  UnitC = ()
+
+instance UnitC => Functor I where
+  -- The UnitC type family in the context needs UndecidableIntances
+  fmap = undefined
index 4bf7fa0..5887b3c 100644 (file)
@@ -644,3 +644,4 @@ test('T15242', normalise_errmsg_fun(onlyHsParLocs), compile, [''])
 test('T15428', normal, compile, [''])
 test('T15431', normal, compile, [''])
 test('T15431a', normal, compile, [''])
+test('T15412', normal, compile, [''])