Strip casts in checkValidInstHead

This patch addresses Trac #11464.

The fix is a bit crude (traverse the type to remove CastTys),
but it's also simple.

See Note [Casts during validity checking] in TcValidity

compiler/typecheck/TcType.hs

@@ -60,7 +60,6 @@ module TcType (
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcRepSplitTyConApp_maybe,
   tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
-  tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
   tcGetTyVar_maybe, tcGetTyVar, nextRole,
   tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
 
@@ -205,7 +204,6 @@ import Util
 import Bag
 import Maybes
 import Pair
-import ListSetOps
 import Outputable
 import FastString
 import ErrUtils( Validity(..), MsgDoc, isValid )
@@ -1259,39 +1257,6 @@ tcSplitDFunTy ty
 tcSplitDFunHead :: Type -> (Class, [Type])
 tcSplitDFunHead = getClassPredTys
 
-tcInstHeadTyNotSynonym :: Type -> Bool
--- Used in Haskell-98 mode, for the argument types of an instance head
--- These must not be type synonyms, but everywhere else type synonyms
--- are transparent, so we need a special function here
-tcInstHeadTyNotSynonym ty
-  = case ty of
-        TyConApp tc _ -> not (isTypeSynonymTyCon tc)
-        _ -> True
-
-tcInstHeadTyAppAllTyVars :: Type -> Bool
--- Used in Haskell-98 mode, for the argument types of an instance head
--- These must be a constructor applied to type variable arguments.
--- But we allow kind instantiations.
-tcInstHeadTyAppAllTyVars ty
-  | Just ty' <- coreView ty       -- Look through synonyms
-  = tcInstHeadTyAppAllTyVars ty'
-  | otherwise
-  = case ty of
-        TyConApp tc tys         -> ok (filterOutInvisibleTypes tc tys)
-           -- avoid kinds
-
-        ForAllTy (Anon arg) res -> ok [arg, res]
-        _                       -> False
-  where
-        -- Check that all the types are type variables,
-        -- and that each is distinct
-    ok tys = equalLength tvs tys && hasNoDups tvs
-           where
-             tvs = mapMaybe get_tv tys
-
-    get_tv (TyVarTy tv)  = Just tv      -- through synonyms
-    get_tv _             = Nothing
-
 tcEqKind :: TcKind -> TcKind -> Bool
 tcEqKind = tcEqType
 

compiler/typecheck/TcValidity.hs

@@ -1009,6 +1009,48 @@ checkValidInstHead ctxt clas cls_args
     abstract_class_msg =
                 text "Manual instances of this class are not permitted."
 
+tcInstHeadTyNotSynonym :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must not be type synonyms, but everywhere else type synonyms
+-- are transparent, so we need a special function here
+tcInstHeadTyNotSynonym ty
+  = case ty of  -- Do not use splitTyConApp,
+                -- because that expands synonyms!
+        TyConApp tc _ -> not (isTypeSynonymTyCon tc)
+        _ -> True
+
+tcInstHeadTyAppAllTyVars :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must be a constructor applied to type variable arguments.
+-- But we allow kind instantiations.
+tcInstHeadTyAppAllTyVars ty
+  | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
+  = ok (filterOutInvisibleTypes tc tys)  -- avoid kinds
+
+  | otherwise
+  = False
+  where
+        -- Check that all the types are type variables,
+        -- and that each is distinct
+    ok tys = equalLength tvs tys && hasNoDups tvs
+           where
+             tvs = mapMaybe tcGetTyVar_maybe tys
+
+dropCasts :: Type -> Type
+-- See Note [Casts during validity checking]
+-- This function can turn a well-kinded type into an ill-kinded
+-- one, so I've kept it local to this module
+-- To consider: drop only UnivCo(HoleProv) casts
+dropCasts (CastTy ty _)     = dropCasts ty
+dropCasts (AppTy t1 t2)     = mkAppTy (dropCasts t1) (dropCasts t2)
+dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
+dropCasts (ForAllTy b ty)   = ForAllTy (dropCastsB b) (dropCasts ty)
+dropCasts ty                = ty  -- LitTy, TyVarTy, CoercionTy
+
+dropCastsB :: TyBinder -> TyBinder
+dropCastsB (Anon ty) = Anon (dropCasts ty)
+dropCastsB b         = b   -- Don't bother in the kind of a forall
+
 abstractClassKeys :: [Unique]
 abstractClassKeys = [ heqTyConKey
                     , eqTyConKey
@@ -1021,8 +1063,23 @@ instTypeErr cls tys msg
              2 (quotes (pprClassPred cls tys)))
        2 msg
 
-{- Note [Valid 'deriving' predicate]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Casts during validity checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the (bogus)
+     instance Eq Char#
+We elaborate to  'Eq (Char# |> UnivCo(hole))'  where the hole is an
+insoluble equality constraint for * ~ #.  We'll report the insoluble
+constraint separately, but we don't want to *also* complain that Eq is
+not applied to a type constructor.  So we look gaily look through
+CastTys here.
+
+Another example:  Eq (Either a).  Then we actually get a cast in
+the middle:
+   Eq ((Either |> g) a)
+
+
+Note [Valid 'deriving' predicate]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 validDerivPred checks for OK 'deriving' context.  See Note [Exotic
 derived instance contexts] in TcDeriv.  However the predicate is
 here because it uses sizeTypes, fvTypes.

testsuite/tests/typecheck/should_fail/T11464.hs

+{-# LANGUAGE MagicHash, PolyKinds #-}
+
+module Foo where
+
+instance Eq (Either a)

testsuite/tests/typecheck/should_fail/T11464.stderr

+
+T11464.hs:5:14: error:
+    • Expecting one more argument to ‘Either a’
+      Expected a type, but ‘Either a’ has kind ‘* -> *’
+    • In the first argument of ‘Eq’, namely ‘Either a’
+      In the instance declaration for ‘Eq (Either a)’

testsuite/tests/typecheck/should_fail/all.T

@@ -403,3 +403,4 @@ test('T10619', normal, compile_fail, [''])
 test('T11347', normal, compile_fail, [''])
 test('T11356', normal, compile_fail, [''])
 test('T11355', normal, compile_fail, [''])
+test('T11464', normal, compile_fail, [''])