#8799 closed feature request (fixed)
Orientation of given `Coercible` constraints
Reported by: | nomeata | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.6.3 |
Keywords: | Cc: | goldfire | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T8799 |
Blocked By: | Blocking: | ||
Related Tickets: | #8555 | Differential Rev(s): | |
Wiki Page: |
Description
Prelude> :m + GHC.Exts Prelude GHC.Exts> let f :: Coercible a b => b -> a ; f = coerce <interactive>:3:40: Could not coerce from ‛b’ to ‛a’ because ‛b’ and ‛a’ are different types. arising from a use of ‛coerce’ from the context (Coercible a b) bound by the type signature for f :: Coercible a b => b -> a at <interactive>:3:10-32 In the expression: coerce In an equation for ‛f’: f = coerce
Something better could be done here (but its not clear what exactly, and to what general extend).
Change History (6)
comment:1 Changed 4 years ago by
comment:2 Changed 4 years ago by
FWIW this works (with ScopedTypeVariables):
let f :: forall a b. Coercible a b => b -> a; f = coerce (id :: a -> a)
comment:3 Changed 3 years ago by
Cc: | goldfire added |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Due to Richard’s rewrite of the Coercible parser, this now works.
comment:5 Changed 3 years ago by
Test Case: | → typecheck/should_compile/T8799 |
---|
comment:6 Changed 23 months ago by
For future reference:
commit 0cc47eb90805f3e166ac4d3991e66d3346ca05e7
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
Note: See
TracTickets for help on using
tickets.
There is similar behavior when trying to test transitivity. I don't have any suggestions of how to fix this without a whole lot of work.