[GHC] #12919: Equality not used for substitution
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code {{{ {-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-} 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: {{{ Op.hs:20: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 Op.hs:19:9 • In the expression: Dict In an equation for ‘prop’: prop = Dict • Relevant bindings include prop :: Dict VF xs f ~ f (bound at Op.hs:20: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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 *** }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire @@ -6,0 +6,2 @@ + module T12919 where + @@ -8,1 +10,1 @@ - data N = Z + data Nat = Z @@ -10,2 +12,2 @@ - data V :: N -> Type where - VZ :: V Z + data D :: Nat -> Type where + DZ :: D Z @@ -13,1 +15,1 @@ - type family VC (n :: N) :: Type where + type family VC (n :: Nat) :: Type where @@ -16,2 +18,2 @@ - type family VF (xs :: V n) (f :: VC n) :: Type where - VF VZ f = f + type family VF (xs :: D n) (f :: VC n) :: Type where + VF DZ f = f @@ -22,1 +24,1 @@ - prop :: xs ~ VZ => Dict (VF xs f ~ f) + prop :: xs ~ DZ => Dict (VF xs f ~ f) New description: This code {{{ {-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-} module T12919 where import Data.Kind data Nat = Z data D :: Nat -> Type where DZ :: D Z type family VC (n :: Nat) :: Type where VC Z = Type type family VF (xs :: D n) (f :: VC n) :: Type where VF DZ f = f data Dict c where Dict :: c => Dict c prop :: xs ~ DZ => Dict (VF xs f ~ f) prop = Dict }}} fails with this error: {{{ Op.hs:20: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 Op.hs:19:9 • In the expression: Dict In an equation for ‘prop’: prop = Dict • Relevant bindings include prop :: Dict VF xs f ~ f (bound at Op.hs:20: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. -- Comment: 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)`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType * priority: high => highest -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by int-index: @@ -10,1 +10,1 @@ - data Nat = Z + data N = Z @@ -12,2 +12,2 @@ - data D :: Nat -> Type where - DZ :: D Z + data V :: N -> Type where + VZ :: V Z @@ -15,1 +15,1 @@ - type family VC (n :: Nat) :: Type where + type family VC (n :: N) :: Type where @@ -18,2 +18,2 @@ - type family VF (xs :: D n) (f :: VC n) :: Type where - VF DZ f = f + type family VF (xs :: V n) (f :: VC n) :: Type where + VF VZ f = f @@ -24,1 +24,1 @@ - prop :: xs ~ DZ => Dict (VF xs f ~ f) + prop :: xs ~ VZ => Dict (VF xs f ~ f) @@ -31,1 +31,1 @@ - Op.hs:20:8: error: + T12919.hs:22:8: error: @@ -37,1 +37,1 @@ - at Op.hs:19:9 + at T12919.hs:21:9 @@ -41,1 +41,1 @@ - prop :: Dict VF xs f ~ f (bound at Op.hs:20:1) + prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1) New description: 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. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"41ec722d71db0eadeddd582a23aab7347349185f/ghc" 41ec722d/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="41ec722d71db0eadeddd582a23aab7347349185f" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * testcase: => typecheck/should_compile/T12919 * milestone: => 8.2.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Goldfire, is there still a chance that this will happen for 8.2? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.1 => 8.4.1 Comment: Alright, bumping off to 8.4. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Much simpler case of what I believe is the same underlying error: #13643. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: #13643 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * related: => #13643 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: #13643 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"8e15e3d370e9c253ae0dbb330e25b72cb00cdb76/ghc" 8e15e3d3/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8e15e3d370e9c253ae0dbb330e25b72cb00cdb76" 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} }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: #13643 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Does this patch fix the panic in #14024? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => patch * differential: => Phab:D3848 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See also #14441, which may be fixed when we commit Phab:D3848. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:17> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): #14556 is also blocked on this ticket. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:20> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Old description:
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.
New description: This code {{{#!hs {-# 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. -- Comment (by bgamari): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Changes (by lelf): * cc: lelf (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"e3dbb44f53b2f9403d20d84e27f187062755a089/ghc" e3dbb44f/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e3dbb44f53b2f9403d20d84e27f187062755a089" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:23> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"b47a6c3a6d9c5da341184824549a6a835c79de15/ghc" b47a6c3/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b47a6c3a6d9c5da341184824549a6a835c79de15" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:24> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: patch => closed * resolution: => fixed Comment: At long, long last, this is put to bed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:25> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12919: Equality not used for substitution -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T12919 Blocked By: | Blocking: 14441 Related Tickets: #13643 | Differential Rev(s): Phab:D3848 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Marge Bot <ben+marge-bot@…>): In [changeset:"2b90356d26b4699227816ad9424e766eccdb6c36/ghc" 2b90356d/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2b90356d26b4699227816ad9424e766eccdb6c36" Fix #14729 by making the normaliser homogeneous This ports the fix to #12919 to the normaliser. (#12919 was about the flattener.) Because the fix is involved, this is done by moving the critical piece of code to Coercion, and then calling this from both the flattener and the normaliser. The key bit is: simplifying type families in a type is always a *homogeneous* operation. See #12919 for a discussion of why this is the Right Way to simplify type families. Also fixes #15549. test case: dependent/should_compile/T14729{,kind} typecheck/should_compile/T15549[ab] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:26> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC