Simplify given `Coercible` constraints

It would be feasible and possibly useful if

foo :: Coercible [a] [b] => a -> b
foo = coerce

would work. This involve simplifying CtGivens similar to how given (nominal) equalities are simplified.

I’ll defer working on this, as it is not strictly required, it seems.

Trac metadata

Trac field	Value
Version	7.7
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#8503 (closed)
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import typechecker labels

Certainly nothing blocking this at the Core level... the Nth coercion constructor would do the right thing here.

Trac metadata

Trac field	Value
Related	#8503 (closed) → #8503 (closed), #8555 (closed)

assigned to @trac-archblob

This looks like a good place to further my understanding of ghc internals so I'll give it a try if no one else is doing it currently, so if someone is, please say so and don't let me waste my time :-P.

Nobody is working on it, so if you feel like it, please give it a shot. (But also beware that in the last months, nobody was missing the feature, so it may have a limited impact – don’t let that lessen your motivation!)

mentioned in issue #9117 (closed)

mentioned in issue #9118

I doubt that this is very useful in practice. I think there are plenty of other more directly useful tickets. Eg look at wiki:Status/SLPJ-Tickets. For example, #5610 (closed)/#7243 (closed) looks tractable and useful. #8281 looks as if it needs a push. Etc.

Simon

Yeah, I am more interested in the typechecker part of ghc at the moment, so I just chose something recent. I'll certainly have a lookt at those tickets and see if I can help. :)

unassigned @trac-archblob

closed

Due to Richards rewrite of the Coercible parser, this now works.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
CC	fcsernik@gmail.com → fcsernik@gmail.com, goldfire

mentioned in commit fc8c5e7a

Trac metadata

Trac field	Value
Test case	→ typecheck/should_compile/T8555

For future reference:

commit 0cc47eb9

Author: Richard Eisenberg <eir@cis.upenn.edu>
Date:   Fri Dec 12 17:19:21 2014 -0500

    Rewrite `Coercible` solver
    
    Summary:
    This is a rewrite of the algorithm to solve for Coercible "instances".
    
    A preliminary form of these ideas is at
    https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver
    
    The basic idea here is that the `EqPred` constructor of `PredTree`
    now is parameterised by a new type `EqRel` (where
    `data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
    now talk about nominal equality (the usual case) or representational
    equality (the `Coercible` case).
    
    This is a change from the previous
    behavior where `Coercible` was just considered a regular class with
    a special case in `matchClassInst`.
    
    Because of this change, representational equalities are now
    canonicalized just like nominal ones, allowing more equalities
    to be solved -- in particular, the case at the top of #9117.
    
    A knock-on effect is that the flattener must be aware of the
    choice of equality relation, because the inert set now stores
    both representational inert equalities alongside the nominal
    inert equalities. Of course, we can use representational equalities
    to rewrite only within another representational equality --
    thus the parameterization of the flattener.
    
    A nice side effect of this change is that I've introduced a new
    type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
    in the flattener.
    
    This commit includes some refactoring as discussed on D546.
    It also removes the ability of Deriveds to rewrite Deriveds.
    
    This fixes bugs #9117 and #8984.
    
    Reviewers: simonpj, austin, nomeata
    
    Subscribers: carter, thomie
    
    Differential Revision: https://phabricator.haskell.org/D546
    
    GHC Trac Issues: #9117, #8984

added Pnormal label