Revert "Remove unnecessary isTyVar tests in TcType"
authorRyan Scott <ryan.gl.scott@gmail.com>
Sun, 22 Jan 2017 17:57:08 +0000 (12:57 -0500)
committerRyan Scott <ryan.gl.scott@gmail.com>
Sun, 22 Jan 2017 17:57:09 +0000 (12:57 -0500)
Summary:
This reverts commit a0899b2f66a4102a7cf21569889381446ce63833. This is because
removing these checks prompts panics in at least two different programs
reported in #12785.

Test Plan: ./validate

Reviewers: simonpj, goldfire, bgamari, austin

Subscribers: thomie

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

GHC Trac Issues: #12785

compiler/typecheck/TcType.hs
testsuite/tests/typecheck/should_compile/T12785a.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_fail/T12785b.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T12785b.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 48a2f06..41a5bdd 100644 (file)
@@ -298,6 +298,18 @@ This is a bit of a change from an earlier era when we remoselessly
 insisted on real TcTyVars in the type checker.  But that seems
 unnecessary (for skolems, TyVars are fine) and it's now very hard
 to guarantee, with the advent of kind equalities.
+
+Note [Coercion variables in free variable lists]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are several places in the GHC codebase where functions like
+tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type
+variables of a type. The "Co" part of these functions' names shouldn't be
+dismissed, as it is entirely possible that they will include coercion variables
+in addition to type variables! As a result, there are some places in TcType
+where we must take care to check that a variable is a _type_ variable (using
+isTyVar) before calling tcTyVarDetails--a partial function that is not defined
+for coercion variables--on the variable. Failing to do so led to
+GHC Trac #12785.
 -}
 
 -- See Note [TcTyVars in the typechecker]
@@ -1065,6 +1077,7 @@ isTouchableOrFmv ctxt_tclvl tv
 
 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
 isTouchableMetaTyVar ctxt_tclvl tv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
       MetaTv { mtv_tclvl = tv_tclvl }
@@ -1072,13 +1085,16 @@ isTouchableMetaTyVar ctxt_tclvl tv
                     ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
            tv_tclvl `sameDepthAs` ctxt_tclvl
       _ -> False
+  | otherwise = False
 
 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
 isFloatedTouchableMetaTyVar ctxt_tclvl tv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
       MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
       _ -> False
+  | otherwise = False
 
 isImmutableTyVar :: TyVar -> Bool
 isImmutableTyVar tv = isSkolemTyVar tv
@@ -1091,10 +1107,12 @@ isTyConableTyVar tv
         -- True of a meta-type variable that can be filled in
         -- with a type constructor application; in particular,
         -- not a SigTv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
         MetaTv { mtv_info = SigTv } -> False
         _                           -> True
+  | otherwise = True
 
 isFmvTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
@@ -1124,16 +1142,20 @@ isSkolemTyVar tv
         _other    -> True
 
 isOverlappableTyVar tv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
         SkolemTv _ overlappable -> overlappable
         _                       -> False
+  | otherwise = False
 
 isMetaTyVar tv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
         MetaTv {} -> True
         _         -> False
+  | otherwise = False
 
 -- isAmbiguousTyVar is used only when reporting type errors
 -- It picks out variables that are unbound, namely meta
@@ -1141,10 +1163,12 @@ isMetaTyVar tv
 -- RtClosureInspect.zonkRTTIType.  These are "ambiguous" in
 -- the sense that they stand for an as-yet-unknown type
 isAmbiguousTyVar tv
+  | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = case tcTyVarDetails tv of
         MetaTv {}     -> True
         RuntimeUnk {} -> True
         _             -> False
+  | otherwise = False
 
 isMetaTyVarTy :: TcType -> Bool
 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
diff --git a/testsuite/tests/typecheck/should_compile/T12785a.hs b/testsuite/tests/typecheck/should_compile/T12785a.hs
new file mode 100644 (file)
index 0000000..1e4d6a1
--- /dev/null
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+module T12785a where
+
+import Data.Kind (Type)
+
+foo :: forall (dk :: Type) (c :: Type -> Type) (t :: dk -> Type) (a :: Type).
+       (dk ~ Type)
+    => (forall (d :: dk). c (t d)) -> Maybe (c a)
+foo _ = Nothing
index 465d8ac..d322cc0 100644 (file)
@@ -559,6 +559,7 @@ test('T12507', normal, compile, [''])
 test('T12734', normal, compile, [''])
 test('T12734a', normal, compile_fail, [''])
 test('T12763', normal, compile, [''])
+test('T12785a', normal, compile, [''])
 test('T12797', normal, compile, [''])
 test('T12911', normal, compile, [''])
 test('T12925', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.hs b/testsuite/tests/typecheck/should_fail/T12785b.hs
new file mode 100644 (file)
index 0000000..4188e3e
--- /dev/null
@@ -0,0 +1,38 @@
+{-# LANGUAGE RankNTypes, TypeInType, TypeOperators, KindSignatures, ViewPatterns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, GADTs #-}
+
+module T12785b where
+
+import Data.Kind
+
+data Peano = Z | S Peano
+
+data HTree n a where
+  Point :: a -> HTree Z a
+  Leaf :: HTree (S n) a
+  Branch :: a -> HTree n (HTree (S n) a) -> HTree (S n) a
+
+data STree n :: forall a . (a -> *) -> HTree n a -> * where
+  SPoint :: f a -> STree Z f (Point a)
+  SLeaf :: STree (S n) f Leaf
+  SBranch :: f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru)
+  SBranchX :: (Payload (S n) (Payload n stru) ~ a)
+          => f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru)
+
+data Hidden :: Peano -> (a -> *) -> * where
+  Hide :: STree n f s -> Hidden n f
+
+nest :: HTree m (Hidden (S m) f) -> Hidden m (STree ('S m) f)
+nest (Point (Hide st)) = Hide (SPoint st)
+nest Leaf = Hide SLeaf
+nest (Hide a `Branch` (nest . hmap nest -> Hide tr)) = Hide $ a `SBranchX` tr
+
+hmap :: (x -> y) -> HTree n x -> HTree n y
+hmap f (Point a) = Point (f a)
+hmap f Leaf = Leaf
+hmap f (a `Branch` tr) = f a `Branch` hmap (hmap f) tr
+
+type family Payload (n :: Peano) (s :: HTree n x) where
+  Payload Z (Point a) = a
+  Payload (S n) (a `Branch` stru) = a
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
new file mode 100644 (file)
index 0000000..0290cfe
--- /dev/null
@@ -0,0 +1,26 @@
+
+T12785b.hs:29:63: error:
+    • Could not deduce: Payload ('S n1) (Payload n1 s1) ~ s
+        arising from a use of ‘SBranchX’
+      from the context: m1 ~ 'S n1
+        bound by a pattern with constructor:
+                   Branch :: forall a (n :: Peano).
+                             a -> HTree n (HTree ('S n) a) -> HTree ('S n) a,
+                 in an equation for ‘nest’
+        at T12785b.hs:29:7-51
+    • In the second argument of ‘($)’, namely ‘a `SBranchX` tr’
+      In the expression: Hide $ a `SBranchX` tr
+      In an equation for ‘nest’:
+          nest (Hide a `Branch` (nest . hmap nest -> Hide tr))
+            = Hide $ a `SBranchX` tr
+    • Relevant bindings include
+        tr :: STree
+                n1
+                (HTree ('S n1) (HTree ('S ('S n1)) a))
+                (STree ('S n1) (HTree ('S ('S n1)) a) (STree ('S ('S n1)) a f))
+                s1
+          (bound at T12785b.hs:29:49)
+        a :: STree ('S m1) a f s (bound at T12785b.hs:29:12)
+        nest :: HTree m1 (Hidden ('S m1) f)
+                -> Hidden m1 (STree ('S m1) a f)
+          (bound at T12785b.hs:27:1)
index 9931037..f4db8ba 100644 (file)
@@ -428,6 +428,7 @@ test('T12124', normal, compile_fail, [''])
 test('T12589', normal, compile_fail, [''])
 test('T12529', normal, compile_fail, [''])
 test('T12729', normal, compile_fail, [''])
+test('T12785b', normal, compile_fail, [''])
 test('T12803', normal, compile_fail, [''])
 test('T12042', extra_clean(['T12042a.hi', 'T12042a.o', 'T12042.hi-boot', 'T12042.o-boot']), multimod_compile_fail, ['T12042', ''])
 test('T12966', normal, compile_fail, [''])