#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Description changed by glguy: Old description:

Hello, I ran into what appears to be a regression in the Coercible solver since 7.8.4. This is as small as I've managed to get my example case.

{{{ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleContexts #-} module Bug where

import Control.Applicative import Data.Coerce

broken :: Bizarre (->) w => w a b t -> () broken = getConst #. bazaar (Const #. const ())

class Profunctor p where (#.) :: Coercible c b => (b -> c) -> p a b -> p a c

class Bizarre p w | w -> p where bazaar :: Applicative f => p a (f b) -> w a b t -> f t }}}

{{{ Bug.hs:10:36: Couldn't match representation of type ‘()’ with that of ‘Const () b’ Relevant role signatures: type role Const representational phantom Relevant bindings include broken :: w a b t -> () (bound at Bug.hs:10:1) In the first argument of ‘bazaar’, namely ‘(Const #. const ())’ In the second argument of ‘(#.)’, namely ‘bazaar (Const #. const ())’ In the expression: getConst #. bazaar (Const #. const ()) }}}

New description: Hello, I ran into what appears to be a regression in the Coercible solver since 7.8.4. This is as small as I've managed to get my example case. {{{ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleContexts #-} module Bug where import Control.Applicative import Data.Coerce broken :: Bizarre (->) w => w a b t -> () broken = getConst #. bazaar (Const #. const ()) class Profunctor p where (#.) :: Coercible c b => (b -> c) -> p a b -> p a c instance Profunctor (->) where (#.) = (.) class Bizarre p w | w -> p where bazaar :: Applicative f => p a (f b) -> w a b t -> f t }}} {{{ Bug.hs:10:36: Couldn't match representation of type ‘()’ with that of ‘Const () b’ Relevant role signatures: type role Const representational phantom Relevant bindings include broken :: w a b t -> () (bound at Bug.hs:10:1) In the first argument of ‘bazaar’, namely ‘(Const #. const ())’ In the second argument of ‘(#.)’, namely ‘bazaar (Const #. const ())’ In the expression: getConst #. bazaar (Const #. const ()) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire Comment: Richard, this is in your bailiwick. The problem is in `TcCanonical`: {{{ -- When working with ReprEq, unwrap newtypes next. -- Otherwise, a ~ Id a wouldn't get solved can_eq_nc' rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2 | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2 can_eq_nc' rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _ | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1 }}} This is done before flattening. At that stage the constaint looks like `Coercible a (f b)`, but we already know `a := ()` `f := Const ()`, so the equation doesn't match. But then we don't see the newtype expansion at all. I suppose we have to flatten ''before'' trying the newtype expansion. Which is a bit awkward in practice. I suspect that we should have a new invariant for `CTyEqCan`, that in canonical constraint `a ~R ty`, the rhs `ty` is never a saturated newtype application. And then enforce that invariant. That would deal with the `CTyEqCan` case. Then we need to do something in `try_decompose_repr_app`. (Acutally that function looks wrong to me. Suppose we had `f Age ~R g Int`. Then if `f` and `g` both flattened to `Maybe` we should decompose, not fail.) This is an outright bug; must fix for 7.10. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by goldfire): I'm on it right this minute, actually. Seems quite straightforward to solve. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"befe2d7c8902096dd184ebca3f7f135ee5f479e8/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="befe2d7c8902096dd184ebca3f7f135ee5f479e8" Fix #10079 by recurring after flattening exposes a TyConApp. Previously, try_decompose_nom_app was smart enough to recur if flattening exposed a TyConApp, but try_decompose_repr_app was not. Now, if neither type in try_decompose_repr_app is an AppTy, recur. Seems all straightforward enough to avoid a Note. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): I'm not sure this is right yet. '''First''' * For some reason `can_eq_nc'` only calls `can_eq_wanted_app` in the wanted/derived case. * That means that `try_decompose_app` cannot assume that its arg types are flattened. But `try_decompose_nom_app` and `try_decompose_repr_app` seem to assume that the type ''is'' flattened. The simple thing would be to rename `can_eq_wanted_app` to `can_eq_app`, and call it in all cases. '''Second'''. In your new `try_decompose_repr_app` you fail if either is an `AppTy`. But what about {{{ f a ~R g f a }}} where `g` flattens to `N`, a newtype {{{ newtype N f a = MkN (f a) }}} Then the flattened version will be {{{ f a ~R N f a }}} and that is certainly soluble. '''Third'''. What about {{{ a ~ f a }}} where `f` flattens to `N2` and {{{ newtype N2 a = MkN2 a }}} At the moment we will miss this altogether. We want an invariant that a representational `CTyEqCan` has a right-hand side that is not a newtype application. And we need to ensure that the invariant holds. So this really doesn't look good yet. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): No I can't remember why the inherited thing was done; but I think we can simplify it away anyway. Re new proposal, I'm worried about what happens if we have `f a ~ N b`, where N's data constructor is not in scope. Then the `tcTopNormaliseNewTypeNF_maybe` thing won't fire, and we'll drop back into the `AppTy` case.... infinite loop. It doesn't smell good... code is too tricky. You don't comment about '''Third''' above; but it's another bug waiting to happen, isn't it? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Changes (by goldfire): * owner: goldfire => * priority: highest => high * differential: => Phab:D653 * resolution: fixed => * status: closed => new Comment: Sadly, Simon's comment:9 exposes some serious flaws in my approach here. Work in progress on the solution is at Phab:D653. (Happily, that solution will also fix #7788 and #8550.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): Er, woops. I didn't mean to delete those changes. We commented at the same time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: For what it's worth, the fix just merged in ''does'' fix the problem stated in the ticket, and it doesn't make any of the issues from comment:9 worse. There's just lots more room for improvement. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by simonpj): Richard, are you proposing to merge the current (incomplete) change to 7.10, leaving the "plan going forward" for 7.12? Or can you do it for 7.10? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by simonpj): Richard has now completed a draft, at Phab:D653, but it's pretty big, and is unlikely to carry over to the 7.10 branch without a lot of fuss (and hence potential errors). Austin will try and report. But otherwise we may just have to do without it. We are very far down the road to 7.10 and I don't want to destablise it. Is that too terrible? (Edward esp.) Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by goldfire): I'm stalled here. :( The work I've done in Phab:D653 works quite well on fixing the bugs listed there, but it fails utterly if it sees a recursive newtype. Consider test case typecheck/should_compile/tc159: {{{ newtype A = A [A] deriving (Eq) }}} GHC naturally tries to use GND here but then gives up when it can't flatten `A` w.r.t. representational equality. Before Phab:D653, this case was handled by the `rec_nts` trick -- a newtype could be unwrapped only once. The problem with this trick is that it makes type inference a little wonky: canonicalization wasn't idempotent! For example, canonicalizing `Coercible skolem A` would get you `Coercible skolem [A]`. Canonicalizing again would give you `Coercible skolem [[A]]` and so on. Putting the `rec_nts` logic in the flattener would make that algorithm non-idempotent. This seems bad. I've flailed around looking for a solution but am coming up dry. (The solution was around this idea: if flattening were stuck in a loop, just return the original unflattened type. This didn't work out in practice, though, because usually the first few steps of flattening were not loopy (i.e., following filled tyvars) and then the flattener would loop. But detecting the loop isn't exactly straightforward.) I see a few possible ways forward: - Accept that representational equality simply omits recursive newtypes. This means that `Note [Recursive newtypes]` in !TcDeriv would have to change, and some programs that compile today would fail to do so. - Continue to use the `rec_nts` trick, meaning that the flattener is not idempotent. Recursive newtypes will still be problematic, though, because the canonicalizer will see a newtype, try to flatten it away, partially succeed (unwrapping one level) and then loop, doing the same thing. Somehow, the canonicalizer would have to be taught not to do this. - Give up on moving unwrapping newtypes into the flattener and devise another way to fix comment:9. The flattener would retain the code I've put there to track type function depths, still fixing some of the tickets listed in comment:22. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by simonpj): Richard and I had a Skype chat. Conclusions: * We worked out what to do about Phab:D653, but there are lots of changes, and 7.10 is very close. * Edward's 117 coerces are already fixed, in 7.10 (see comment:14) * So we will not fix anything further in 7.10. * That leaves un-done the right fix for this ticket (hence some lurking bugs). * Also remaining un-done are #7788, #8550, #9554, and #10139. However none are blocking correct code from compiling and running. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:26 hvr]:

Replying to [comment:25 simonpj]:

... will the known issues resulting from leaving some stuff deliberately unfixed in 7.10 make it into a release-note entry?

I think this is reasonable. I've written up such a note at Phab:D735. O, you with ghc-7.10 access, please merge! Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa" Do proper depth checking in the flattener to avoid looping. This implements (roughly) the plan put forward in comment:14:ticket:7788, fixing #7788, #8550, #9554, #10139, and addressing concerns raised in #10079. There are some regressions w.r.t. GHC 7.8, but only with pathological type families (like F a = F a). This also (hopefully -- don't have a test case) fixes #10158. Unsolved problems include #10184 and #10185, which are both known deficiencies of the approach used here. As part of this change, the plumbing around detecting infinite loops has changed. Instead of -fcontext-stack and -ftype-function-depth, we now have one combined -freduction-depth parameter. Setting it to 0 disbales the check, which is now the recommended way to get (terminating) code to typecheck in releases. (The number of reduction steps may well change between minor GHC releases!) This commit also introduces a new IntWithInf type in BasicTypes that represents an integer+infinity. This type is used in a few places throughout the code. Tests in indexed-types/should_fail/T7788 indexed-types/should_fail/T8550 indexed-types/should_fail/T9554 indexed-types/should_compile/T10079 indexed-types/should_compile/T10139 typecheck/should_compile/T10184 (expected broken) typecheck/should_compile/T10185 (expected broken) This commit also changes performance testsuite numbers, for the better. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler