#7259: Eta expansion of products in System FC
---------------------------------+------------------------------------------
Reporter: simonpj | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone: 7.8.1
Component: Compiler | Version: 7.6.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by adamgundry):
* cc: adam.gundry@… (added)
Comment:
I agree that `Any` should be a type function: to pass kinds as arguments,
the proxy workaround is the right thing for now, at least until we get
explicit type/kind application.
Richard, I think your proposed constraint simplification is sound, but I
don't really understand the advantage over Simon's version. You are
introducing fresh (untouchable?) variables `a1` and `a2` instead of `Fst
a` and `Snd a`, but they don't get you any further. It doesn't matter that
`Fst` and `Snd` are not injective, because the point of the decomposition
into `Fst a ~ t1` and `Snd a ~ t2` is not to solve for `a` (which is
untouchable anyway), but that we might be able to solve for `t1` or `t2`
if one of them is a variable, or we might have other given constraints on
the projections.
In general, adding support for eta to the constraint solver means it
should never get stuck because an inhabitant of a pair (or other record)
kind is not canonical. Certainly type family axioms `F '(a, b) = t` should
be applicable even if the argument is not a canonical pair, but typeclass
instances exhibit the same behaviour. For example, given the definitions
{{{
class Foo (x :: '(a, b))
instance Foo '(a, b)
}}}
we should be able to solve class constraints like `Foo t` using the
existing instance.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7259#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
