Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#10079 closed bug (fixed)

Coercible solver regression: Couldn't match rep of () with Const () b

Reported by: glguy Owned by: goldfire
Priority: high Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.1-rc1
Keywords: Cc: ekmett
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_compile/T10079
Blocked By: Blocking:
Related Tickets: #7788, #8550 Differential Rev(s): Phab:D653
Wiki Page:

Description (last modified by glguy)

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

Change History (32)

comment:1 Changed 3 years ago by glguy

Description: modified (diff)

comment:2 Changed 3 years ago by hvr

Milestone: 7.10.1
Priority: normalhighest

setting high priority to make sure it gets noticed asap for triaging

comment:3 Changed 3 years ago by simonpj

Owner: set to goldfire

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

comment:4 Changed 3 years ago by ekmett

Cc: ekmett added

Thanks, Simon.

We've constructed a workaround for now, but this is pretty much the last thing we have in the way of shedding 117 performance-motivated unsafeCoerce's in favor of coerce. =)

comment:5 Changed 3 years ago by goldfire

I'm on it right this minute, actually. Seems quite straightforward to solve.

comment:6 Changed 3 years ago by goldfire

Yep. Fixed. Will validate and push later today.

try_decompose_repr_app :: CtEvidence
                       -> TcType -> TcType -> TcS (StopOrContinue Ct)
-- Preconditions: like try_decompose_app, but also
--                ev has a representational
try_decompose_repr_app ev ty1 ty2
  | ty1 `eqType` ty2   -- See Note [AppTy reflexivity check]
  = canEqReflexive ev ReprEq ty1

  | AppTy {} <- ty1
  = canEqFailure ev ReprEq ty1 ty2

  | AppTy {} <- ty2
  = canEqFailure ev ReprEq ty1 ty2

  | otherwise  -- flattening in can_eq_wanted_app exposed some TyConApps!
  = ASSERT2( isJust (tcSplitTyConApp_maybe ty1) || isJust (tcSplitTyConApp_maybe ty2)
            , ppr ty1 $$ ppr ty2 )  -- If this assertion fails, we may fall
                                    -- into an infinite loop
    canEqNC ev ReprEq ty1 ty2

comment:7 Changed 3 years ago by Richard Eisenberg <eir@…>

In befe2d7c8902096dd184ebca3f7f135ee5f479e8/ghc:

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.

comment:8 Changed 3 years ago by goldfire

Status: newmerge
Test Case: indexed-types/should_compile/T10079

All set, now.

comment:9 Changed 3 years ago 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

comment:10 in reply to:  9 Changed 3 years ago by goldfire

Replying to simonpj:

I'm not sure this is right yet.

Of course you're right.

The difference in treatment between wanted/deriveds (where we flatten) and givens (where we don't) here is inherited from before my patch. Do you know why this was the case? Regardless, it does seem flattening is always necessary in the representational case.

New proposal: try_decompose_repr_app will recur to canEqNC iff

  1. Either side is headed by a newtype, OR
  2. Neither side is an AppTy.

Should be able to tweak this today.

comment:11 Changed 3 years ago 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

comment:12 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

comment:13 Changed 3 years ago by goldfire

Differential Rev(s): Phab:D653
Owner: goldfire deleted
Priority: highesthigh
Resolution: fixed
Status: closednew

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.)

comment:14 Changed 3 years ago by ekmett

Differential Rev(s): Phab:D653
Priority: highhighest

(As an aside the supplied patch now does enable us to build all of lens unsafeCoerce free.)

@thoughtpolice, is this actually closed, or just had the current patch applied?

I definitely support finding the "right" fix here.

comment:15 Changed 3 years ago by ekmett

Er, woops. I didn't mean to delete those changes. We commented at the same time.

comment:16 Changed 3 years ago by ekmett

Differential Rev(s): Phab:D653
Priority: highesthigh

comment:17 Changed 3 years ago by goldfire

Owner: set to goldfire

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.

comment:18 Changed 3 years ago by goldfire

See comment:14:ticket:7788 for a plan going forward.

comment:19 Changed 3 years ago 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

comment:20 Changed 3 years ago by goldfire

I'm a little squeezed up against the ICFP deadline, on Feb. 27. The plan going forward is a solid half-day's work, I think, which I may not have. When is RC3 due to be cut? I can try to get to it sooner, but having a few days of March would make a big difference for me.

comment:21 Changed 3 years ago 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

comment:22 Changed 3 years ago by goldfire

Just to clarify, the original report with this ticket is actually already fixed in the 7.10 branch (see comment:12). It's just that the fix in 7.10 is very incomplete, as Simon points out in comment:9. That said, the fix in 7.10 doesn't introduce new bad behavior.

So, if we're happy to live with #7788, #8550, #9554, and #10139, then we can avoid merging this to 7.10.

Personally, this is a hard call. If we don't merge, then various (ill-typed) programs will cause GHC to hang, sometimes mysteriously. In particular, #10139 has a program without UndecidableInstances but that hangs 7.10RC2. The patch at Phab:D653 allows the program to compile. But I see how this change could rock the boat! I certainly welcome other opinions about how to proceed.

comment:23 Changed 3 years ago 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?

comment:24 in reply to:  23 Changed 3 years ago by simonpj

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].

I don't agree. Looking at HEAD, I see

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

This case simply won't fire on Coercible skolem [A]. The HEAD does not aggressively unwrap newtypes deep inside types, only immediately under a Coercible. And that's what we should do in the new version too.

Simon

comment:25 Changed 3 years ago 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.

comment:26 in reply to:  25 ; Changed 3 years ago by hvr

Replying to simonpj:

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

comment:27 in reply to:  26 Changed 3 years ago by goldfire

Replying to hvr:

Replying to 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.

comment:28 Changed 3 years ago by goldfire

I've hit a real roadblock here and am stalled. See this wiki page.

comment:29 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone.

comment:30 Changed 3 years ago by Richard Eisenberg <eir@…>

In c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa/ghc:

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.

comment:31 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed

comment:32 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

Note: See TracTickets for help on using tickets.