Opened 8 months ago

Last modified 3 months ago

#12919 new bug

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:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T12919
Blocked By: Blocking:
Related Tickets: #13643 Differential Rev(s):
Wiki Page:

Description (last modified by int-index)

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 (13)

comment:1 Changed 8 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 8 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 8 months ago by simonpj

Keywords: TypeInType added
Priority: highhighest

comment:4 Changed 8 months ago by int-index

Description: modified (diff)

comment:5 Changed 8 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 8 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 8 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 8 months ago by bgamari

Milestone: 8.2.1
Test Case: typecheck/should_compile/T12919

comment:9 Changed 4 months ago by bgamari

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

comment:10 Changed 4 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 4 months ago by bgamari

Milestone: 8.2.18.4.1

Alright, bumping off to 8.4.

comment:12 Changed 3 months ago by goldfire

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

comment:13 Changed 3 months ago by goldfire

Note: See TracTickets for help on using tickets.