Opened 5 months ago
Closed 3 months ago
#13333 closed bug (fixed)
Typeable regression in GHC HEAD
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | highest | Milestone: | 8.2.1 |
Component: | Compiler (Type checker) | Version: | 8.1 |
Keywords: | typeable, TypeInType | Cc: | bgamari, goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | typecheck/should_compile/T13333 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D3424 | |
Wiki Page: |
Description (last modified by )
I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded Typeable
. This compiles without issue on GHC 8.0.1 and 8.0.2:
{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module DataCast where import Data.Data import GHC.Exts (Constraint) data T (phantom :: k) = T data D (p :: k -> Constraint) (x :: j) where D :: forall (p :: k -> Constraint) (x :: k). p x => D p x class Possibly p x where possibly :: proxy1 p -> proxy2 x -> Maybe (D p x) dataCast1T :: forall k c t (phantom :: k). (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom) => (forall d. Data d => c (t d)) -> Maybe (c (T phantom)) dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of Nothing -> Nothing Just D -> gcast1 f
But on GHC HEAD, it barfs this error:
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling DataCast ( Bug.hs, interpreted ) Bug.hs:28:29: error: • Could not deduce (Typeable T) arising from a use of ‘gcast1’ GHC can't yet do polykinded Typeable (T :: * -> *) from the context: (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom) bound by the type signature for: dataCast1T :: (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom) => (forall d. Data d => c (t d)) -> Maybe (c (T phantom)) at Bug.hs:(22,1)-(25,35) or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x) bound by a pattern with constructor: D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x, in a case alternative at Bug.hs:28:23 • In the expression: gcast1 f In a case alternative: Just D -> gcast1 f In the expression: case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of Nothing -> Nothing Just D -> gcast1 f | 28 | Just D -> gcast1 f | ^^^^^^^^
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded Typeable
nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.
Change History (18)
comment:1 Changed 5 months ago by
Description: | modified (diff) |
---|
comment:2 Changed 5 months ago by
comment:3 Changed 5 months ago by
Keywords: | typeable added |
---|
comment:4 Changed 4 months ago by
Owner: | set to bgamari |
---|
comment:5 Changed 4 months ago by
Looking at -ddump-tc-trace
from the program in the ticket description, it seems that we are failing to solve for this,
WC {wc_simple = [WD] $dTypeable_a29a {0}:: Typeable (T |> Trans (Sym cobox ->_N <*>_N) (cobox ->_N <*>_N)) (CDictCan)}
I believe the reason for this is that we don't handle casts in the Typeable
solver. I'll need to think about this.
comment:6 Changed 4 months ago by
I think that if we have t :: k1
and c :: k1 ~ k2
and
Constraints: [W] c :: Typeable k2 (t |> c)
then we can simplify the wanted constraint to
Bindings: c = c1 |> Typeable ?? c Constraints: [W] c1 :: Typeable k1 t
Richard do you agree? What is the ??
?
comment:7 Changed 4 months ago by
Also what if we have
Eq (t |> c)
Can we solve that, or do we get stuck?
comment:8 Changed 4 months ago by
I have a solution in progress. But no time to finish now. Soon. It involves adding a case for casts in matchTypeable
. Not hard.
comment:9 Changed 3 months ago by
Differential Rev(s): | → Phab:D3424 |
---|
I now think I know what's going on here, but unsure the best way to fix it. Interestingly, the problem has nothing to do with Typeable
or TypeInType
. Indeed it's amazing we've never hit this problem before.
We have
[G] c1 :: k1[tau] ~ j1[tau]
in an implication. Both k1
and j1
are filled in at this point: k1 := Type
and j1 := k2[sk]
. This constraint is then passed through solveSimpleGivens
, where it is canonicalized. can_eq_nc'
flattens both sides, following both k1
and j1
to find Type
. can_eq_nc'
then calls rewriteEqEvidence
which creates a new
[G] c2 :: Type ~ k2[sk]
Of course, GHC produces evidence for c2
: c2 = g1 ; c1 ; g2
, where g1
and g2
are the coercions that come from flattening k1
and j1
.
The problem is that these coercions, g1
and g2
are both reflexive, as they arise simply from zonking. See the line of code here. When c2
is stitched together from g1
, c1
, and g2
, the calls to mkTcTransCo
notice that some of the arguments are Refl
, and so ignores the reflexive arguments. The end result is that c2 = c1
. And then, when c2
gets put in the inert set, its kind still mentions unzonked variables. (Even though the associated ctPred
is just fine.)
What to do? Here are some ideas:
- Stop
mkTcTransCo
(but notmkTransCo
) from optimizing this case.
- Add a zonk somewhere (
addInertEq
? seems better thanrewriteEqEvidence
) to fix this problem.
- Add a new coercion form
ZonkCo
that relates an unzonked tyvar to its contents. This way, we can have the invariant that, whenever(ty', co) <- flatten ty
, we haveco :: ty' ~ ty
. (Right now, that final equality is true only modulo zonking. But the newZonkCo
would allow it to be true without needing to zonk.) In fully-typechecked Core,ZonkCo
would zonk to become reflexive, and so Core would have noZonkCo
s.
- Add a new
castTcCoercion
function that stitches three coercions together using transitivity; thiscastTcCoercion
would cleverly not optimize theRefl
away.
I favor (1) but am worried about performance implications. (3) is probably the most principled, but it seems like a sledgehammer to tap in a nail. (4) is a middle ground, but I'm worried that what's happening here (a coercion returned from the flattener having an unzonked kind) happens elsewhere where we wouldn't use castTcCoercion
.
What are your thoughts?
(NB: The patch linked to here does not have any of these fixes. I posted that patch some time ago but never added the link from this ticket.)
comment:10 Changed 3 months ago by
The end result is that c2 = c1. And then, when c2 gets put in the inert set, its kind still mentions unzonked variables. (Even though the associated ctPred is just fine.)
I don't see the problem. See Note [Ct/evidence invariant]
in TcRnTypes
. The types in evidence terms are no zonked, and that should not matter one whit.
Can you explain more precisely what actually goes wrong and why?
Simon
comment:11 Changed 3 months ago by
It turns out that Note is no longer true. See Phab:D3424 for more explanation. There are validation failures there I have not investigated yet.
comment:12 Changed 3 months ago by
I'm sorry, but I still don't get it. Why don't we fix the bug that makes the Note untrue? I do not understand why it's bad for an evidence term (which the constraint solver never looks at) to be Refl, if it relates two types that are equal after zonking.
Your diagnosis concludes
And then, when c2 gets put in the inert set, its kind still mentions unzonked variables.
But you do not say why that matters. I think it should not matter.
Can you explain more precisely what goes wrong and why?
comment:13 Changed 3 months ago by
Owner: | changed from bgamari to goldfire |
---|---|
Priority: | high → highest |
Bumping the priority of this; I don't think we'll want to cut an 8.2-rc2 until this is fixed.
comment:14 Changed 3 months ago by
Keywords: | TypeInType added |
---|
comment:15 Changed 3 months ago by
Status: | new → patch |
---|
comment:17 Changed 3 months ago by
Status: | patch → merge |
---|---|
Test Case: | → typecheck/should_compile/T13333 |
Thanks for pushing this, Ben!
comment:18 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged to ghc-8.2
as 51d80c3b2c4c7d8f1f5dbcee39864c2de49143c7.
I've observed something even stranger about this program. Let's tweak it slightly and add a couple more things (note that the definition of
dataCast1T
is unchanged):With GHC HEAD, this gives the same error as the original program. But if you add this one definition to this file:
Then it typechecks without issue on GHC HEAD! This is pretty bizarre, considering that the error was originally reported in
dataCast1T
, and we managed to make the error go away without making a single change todataCast1T
.FWIW, this program also compiles without issue on GHC 8.0.2 (with and without
test1
).