[commit: ghc] master: Strip casts in checkValidInstHead (b2e6350)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/b2e6350fb23403f1c88c5cfed5270d78dbdb6573/ghc

>---------------------------------------------------------------

commit b2e6350fb23403f1c88c5cfed5270d78dbdb6573
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Jan 20 16:04:20 2016 +0000

    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


>---------------------------------------------------------------

b2e6350fb23403f1c88c5cfed5270d78dbdb6573
 compiler/typecheck/TcType.hs                       | 35 -------------
 compiler/typecheck/TcValidity.hs                   | 61 +++++++++++++++++++++-
 testsuite/tests/typecheck/should_fail/T11464.hs    |  5 ++
 .../tests/typecheck/should_fail/T11464.stderr      |  6 +++
 testsuite/tests/typecheck/should_fail/all.T        |  1 +
 5 files changed, 71 insertions(+), 37 deletions(-)

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 1b9ae29..c5edfb5 100644
--- a/compiler/typecheck/TcType.hs
+++ b/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
 
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 21accdb..407a01e 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/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.
diff --git a/testsuite/tests/typecheck/should_fail/T11464.hs b/testsuite/tests/typecheck/should_fail/T11464.hs
new file mode 100644
index 0000000..88246aa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T11464.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE MagicHash, PolyKinds #-}
+
+module Foo where
+
+instance Eq (Either a)
diff --git a/testsuite/tests/typecheck/should_fail/T11464.stderr b/testsuite/tests/typecheck/should_fail/T11464.stderr
new file mode 100644
index 0000000..f340291
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T11464.stderr
@@ -0,0 +1,6 @@
+
+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)’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 88ab499..1c4e86e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/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, [''])