Commit 560bc289 authored by Ryan Scott's avatar Ryan Scott
Browse files

Revert "Remove unnecessary isTyVar tests in TcType"

Summary:
This reverts commit a0899b2f. 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
parent f9ccad23
......@@ -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
......
{-# 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
......@@ -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, [''])
......
{-# 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
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)
......@@ -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, [''])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment