Opened 18 months ago

Closed 8 weeks ago

#12919 closed bug (fixed)

Equality not used for substitution

Reported by: int-index Owned by: goldfire
Priority: highest Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc: lelf
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T12919
Blocked By: Blocking: #14441
Related Tickets: #13643 Differential Rev(s): Phab:D3848
Wiki Page:

Description (last modified by bgamari)

This code

{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}

module T12919 where

import Data.Kind

data N = Z

data V :: N -> Type where
  VZ :: V Z

type family VC (n :: N) :: Type where
  VC Z = Type

type family VF (xs :: V n) (f :: VC n) :: Type where
  VF VZ f = f

data Dict c where
  Dict :: c => Dict c

prop :: xs ~ VZ => Dict (VF xs f ~ f)
prop = Dict

fails with this error:

T12919.hs:22:8: error:
    • Couldn't match type ‘f’ with ‘VF 'VZ f’
        arising from a use of ‘Dict’
      ‘f’ is a rigid type variable bound by
        the type signature for:
          prop :: forall (xs :: V 'Z) f. xs ~ 'VZ => Dict VF xs f ~ f
        at T12919.hs:21:9
    • In the expression: Dict
      In an equation for ‘prop’: prop = Dict
    • Relevant bindings include
        prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1)

However, if I substitute xs with VZ (by hand) in the type of prop, it compiles. Can be reproduced with GHC 8.0.1 but not HEAD.

Change History (25)

comment:1 Changed 18 months ago by int-index

Running the test actually resulted in a Core Lint error:

Compile failed (exit code 1) errors were:
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    [in body of lambda with binder $d~_aEs :: (xs :: V 'Z)
                                              ~
                                              ('VZ :: V 'Z)]
    From-type of Cast differs from type of enclosed expression
    From-type: VC 'Z
    Type of enclosed expr: Type
    Actual enclosed expr: f
    Coercion used in cast: D:R:VC[0]
*** Offending Program ***
prop
  :: forall (xs :: V 'Z) f.
     (xs :: V 'Z) ~ ('VZ :: V 'Z) =>
     Dict (VF xs (f |> Sym (D:R:VC[0])) :: Type) ~ (f :: Type)
[LclIdX]
prop =
  \ (@ (xs_aEp :: V 'Z))
    (@ f_aEq)
    ($d~_aEs :: (xs :: V 'Z) ~ ('VZ :: V 'Z)) ->
    case HEq_sc
           @ (V 'Z) @ (V 'Z) @ xs @ 'VZ ($p1~ @ (V 'Z) @ xs @ 'VZ $d~_aEs)
    of cobox_aEM
    { __DEFAULT ->
    (Dict
       @ (f :: Type) ~ (f :: Type)
       ($f~kab
          @ *
          @ f
          @ f
          (Eq# @ * @ * @ f @ f @~ (<f>_N :: (f :: Type) ~# (f :: Type)))))
    `cast` ((Dict
               ((~)
                  <*>_N
                  (Trans
                       (Sym (D:R:VF[0] (Coh <f>_N (D:R:VC[0]))))
                       (VF
                          <'Z>_N
                          (Sym cobox)
                          (Sym (Coh (Sym (Coh <f>_N <Type>_N)) (Sym (D:R:VC[0])))))_N)
                  <f>_N)_R)_R
            :: (Dict (f :: *) ~ (f :: *) :: *)
               ~R#
               (Dict (VF xs (f |> Sym (D:R:VC[0])) :: *) ~ (f :: *) :: *))
    }

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "T12919"#)

$tc'Z :: TyCon
[LclIdX]
$tc'Z =
  TyCon
    4444267892940526647##
    16578485670798467485##
    $trModule
    (TrNameS "'Z"#)

$tcN :: TyCon
[LclIdX]
$tcN =
  TyCon
    17882793663470508219##
    7927123420536316171##
    $trModule
    (TrNameS "N"#)

$tc'VZ :: TyCon
[LclIdX]
$tc'VZ =
  TyCon
    17982818364639448466##
    3866213651802933295##
    $trModule
    (TrNameS "'VZ"#)

$tcV :: TyCon
[LclIdX]
$tcV =
  TyCon
    2444936942366493139##
    17118784387149548812##
    $trModule
    (TrNameS "V"#)

$tc'Dict :: TyCon
[LclIdX]
$tc'Dict =
  TyCon
    12076319013818359472##
    5127630525431558702##
    $trModule
    (TrNameS "'Dict"#)

$tcDict :: TyCon
[LclIdX]
$tcDict =
  TyCon
    8038429513029328469##
    10238893879637068951##
    $trModule
    (TrNameS "Dict"#)

*** End of Offense ***

comment:2 Changed 18 months ago by simonpj

Description: modified (diff)
Owner: set to goldfire

Richard, could you look at this? It's an outright bug. I had a look and my brain melted.

  • We seem to be flattening a type ((f::*) |> Sym D:R:VC[0]), where I think
    axiom D:R:VC[0] :: VC Z ~ Type
    
    But the result of this flattening seems to be ((f:*) |> D:R:VC[0]), which is plainly wrong.
  • I don't understand the code
    flatten_one (CastTy ty g)
      = do { (xi, co) <- flatten_one ty
           ; (g', _) <- flatten_co g
           ; return (mkCastTy xi g', castCoercionKind co g' g) }
    
    It seems suspicious that the evidence returned by flatten_co is discarded.
  • flatten_co is inadequately commented. Perhaps
      If  r is a role
          co :: s ~r t
          flatten_co co = (fco, kco)
    
      then
          fco :: fs ~r ft
          fs, ft are flattened types
          kco :: (fs ~r ft) ~N# (s ~r t)
    
    But I'm really not sure.
  • The flatten_one (CastTy ty g) plan seems quite baroque when applied to ((f::*) |> D:R:VC[0]). Apparently, in flatten_co we
    • Take the coercion D:R:VC[0], and flatten its from-type *, and its to-type VC Z.
    • Flattening its to-type uses Sym D:R:VC[0] to produce * again.
    • So we end up with Refl ; D:R:VC[0] : Sym D:R:VC[0], which seems a bit of a waste.

Generally, could you add a note about flattening (t |> g)?

comment:3 Changed 18 months ago by simonpj

Keywords: TypeInType added
Priority: highhighest

comment:4 Changed 18 months ago by int-index

Description: modified (diff)

comment:5 Changed 18 months ago by goldfire

While I don't see what's going wrong here -- and something surely is -- I'm not as concerned about flatten_co. The second return value from the function is always ignored and should indeed be removed. It is a coercion relating the output coercion to the input, as constructed by mkProofIrrelCo. (Yes, this is a coercion relating two coercions.) These coercions are cheap to make, as any two coercions proving the same proposition are considered equal.

Is this holding you up today? Or is it OK to wait a few weeks? I see the "highest" priority and will surely fix for 8.2.

comment:6 Changed 18 months ago by simonpj

It's not holding me up, but presumably it's holding int-index up, and outright Lint bugs seem so egregious that I try to fix them fast.

comment:7 Changed 18 months ago by Ben Gamari <ben@…>

In 41ec722d/ghc:

Test Trac #12919

Test Plan: make test TEST=T12919

Reviewers: bgamari, austin

Reviewed By: bgamari

Subscribers: thomie

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

GHC Trac Issues: #12919

comment:8 Changed 18 months ago by bgamari

Milestone: 8.2.1
Test Case: typecheck/should_compile/T12919

comment:9 Changed 15 months ago by bgamari

Goldfire, is there still a chance that this will happen for 8.2?

comment:10 Changed 14 months ago by goldfire

I hate to say so, but I doubt it. Fixing this requires making some substantive changes to the flattener (specifically, changing "flattened types have flattened kinds" to "flattening does not change a type's kind"). Making this change in the presence of tycons with kind polymorphism will require some delicate work. It will all add up to more time than I have, I'm afraid. Merging the far simpler D3315 and D3316 patches seems to be hard enough these days. (Though I've finally figured out that my compilation server is acting unreliably, taking up more of my time than I have to offer. Will continue to work locally to get those patches in.)

comment:11 Changed 14 months ago by bgamari

Milestone: 8.2.18.4.1

Alright, bumping off to 8.4.

comment:12 Changed 13 months ago by goldfire

Much simpler case of what I believe is the same underlying error: #13643.

comment:13 Changed 13 months ago by goldfire

comment:14 Changed 10 months ago by Richard Eisenberg <rae@…>

In 8e15e3d3/ghc:

Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}

comment:15 Changed 10 months ago by simonpj

Does this patch fix the panic in #14024?

comment:16 Changed 9 months ago by goldfire

Differential Rev(s): Phab:D3848
Status: newpatch

comment:17 Changed 6 months ago by simonpj

See also #14441, which may be fixed when we commit Phab:D3848.

comment:18 Changed 6 months ago by simonpj

Blocking: 14441 added

comment:19 Changed 6 months ago by goldfire

For the record: this patch should fix this ticket, #13643, #13822, #14024, #14126, #14038, #13910, #13938. It's hard for me to say how it affects #14441, but Simon's analysis suggests that the problem stems from this ticket as well.

The ticket is held up because of some performance trouble, but we'll get it in eventually.

comment:20 Changed 5 months ago by simonpj

#14556 is also blocked on this ticket.

comment:21 Changed 5 months ago by bgamari

Description: modified (diff)

A brief status update on this: Richard presented me with a patch fixing this a few months ago, giving me the task to reduce its footprint on compiler performance. He provided a few possible avenues for inquiry, a few of which I have explored. The result can be found on the wip/T12919 branch. Unfortunately more performance improvement is necessary as several compiler performance testcases are still regressing in allocations by >50%.

Sadly, I have recently lacked the time to dig back into the issue. Alex Vieth will be picking up the task shortly.

comment:22 Changed 3 months ago by lelf

Cc: lelf added

comment:23 Changed 8 weeks ago by Richard Eisenberg <rae@…>

In e3dbb44f/ghc:

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

comment:24 Changed 8 weeks ago by Richard Eisenberg <rae@…>

In b47a6c3/ghc:

Fix performance of flattener patch (#12919)

This patch, authored by alexvieth and reviewed at D4451,
makes performance improvements by critically optimizing parts
of the flattener.

Summary:
T3064, T5321FD, T5321Fun, T9872a, T9872b, T9872c all pass.
T9872a and T9872c show improvements beyond the -5% threshold.
T9872d fails at 10.9% increased allocations.

comment:25 Changed 8 weeks ago by goldfire

Resolution: fixed
Status: patchclosed

At long, long last, this is put to bed.

Note: See TracTickets for help on using tickets.