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 whereimport Control.Applicativeimport Data.Coercebroken :: 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 cinstance 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 ())
Edited
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
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 solvedcan_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_ty2can_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.)
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. =)
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.
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
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?
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 ticket:10079#comment:96241 worse. There's just lots more room for improvement.
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.
Richard has now completed a draft, at 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.
Just to clarify, the original report with this ticket is actually already fixed in the 7.10 branch (see ticket:10079#comment:96262). It's just that the fix in 7.10 is very incomplete, as Simon points out in ticket:10079#comment:96241. That said, the fix in 7.10 doesn't introduce new bad behavior.
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 (closed) has a program without UndecidableInstances but that hangs 7.10RC2. The patch at 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.
The work I've done in 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 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 ticket:10079#comment:96241. The flattener would retain the code I've put there to track type function depths, still fixing some of the tickets listed in ticket:10079#comment:97204.
Before 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.