#7259: Eta expansion of products in System FC
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by goldfire):
* cc: eir@… (added)
Comment:
Adding some discussion that happened on the email thread:
The axioms that Simon mentioned:
{{{
axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
}}}
The last two axioms are the straightforward compilations of the type
families {{{Fst}}} and {{{Snd}}} -- nothing new is needed to create these.
The first is the challenge and will require some type inference magic.
----
When trying to solve
{{{
[W] (a:'(k1,ks)) ~ '( t1, t2 )
}}}
(where {{{a}}} is untouchable), Simon suggested simplifying to
{{{
[W] '(Fst a, Snd a) ~ '( t1, t2)
}}}
I don't think that's the right replacement. The next natural step would be
decomposition, leading to {{{(Fst a ~ t1)}}} and {{{(Snd a ~ t2)}}}, which
would then get stuck, because {{{Fst}}} and {{{Snd}}} aren't injective.
So, I would say we need
{{{
a1, a2 fresh
[G] a ~ '(a1, a2)
[W] '(a1, a2) ~ '(t1, t2)
}}}
which would then decompose correctly. As I write this, I'm worried about
that freshness condition... what if {{{a}}} appears multiple times in the
type? We would either need to guarantee that {{{a1}}} and {{{a2}}} are the
same each time, or create new {{{[W]}}} constraints that {{{a1 ~ a1'}}},
etc. But, maybe this is easier in practice than it seems. Type inference
experts?
Simon is a bit concerned about constraints like
{{{
F a ~ e
}}}
where {{{a:'(k1,k2)}}}, and we have a type instance like {{{F '(a,b) = ...
}}}.
It seems to me that the proper eta-expansion (a ~ '(Fst a, Snd a)) would
work here.
----
As for {{{Any}}}, (as Nick pointed out and Iavor elaborated) there is a
workaround that Iavor and I can use involving the promoted version of
{{{
data KindProxy (a :: *) = KindProxy
}}}
to make kind classes and such. So, I think it's OK to relegate {{{Any}}}
to a type function. Objections?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7259#comment:2>
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
