#1496: Newtypes and type families combine to produce inconsistent FC(X) axiom
sets
----------------------------------------+-----------------------------------
Reporter: sorear | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.7
Severity: critical | Resolution:
Keywords: | Difficulty: Unknown
Os: Unknown | Testcase:
Architecture: Unknown |
----------------------------------------+-----------------------------------
Comment (by sorear):
As I see it, the fundamental issue here is that the treatment of newtypes
is inconsistent between Haskell and Core. In Haskell, newtypes are just
cheap data, and they can only be added or removed at the top level of a
type. In FC(X), newtypes are rather more like type level lambdas, and can
be added or removed ''anywhere'' in a type expression as long as the
points where β-conversion occurs are clearly marked with `cast`.
The introduction of generalized newtype deriving complicated this.
Because you can use the newtype function on an arbitrary dictionary, you
can construct any value, including Leibniz equality witnesses, thus
allowing FC(X)'s newtype semantics to escape into the Haskell world.
Many other language features, such as GADTs, associated types, and (I
strongly suspect, but have not been able to prove due to the difficulty
inherent in comprehending them) functional dependencies, were implemented
so as to deeply assume Haskell-98 newtype semantics, and break when
exposed to FC(X) lambda semantics.
So, there are two options.
1. Make Haskell look like FC(X)
We would need to treat newtypes as fully transparent for the purposes of
overlap checks in associated-type and fundep checking, and for GADT
overlap/inaccessibility checking.
2. Make FC(X) look like Haskell
We could add a new kind constructor NCO. (Using the concrete syntax of
the Calculus of Constructions, with *{0} the sort of values and *{1} the
sort of types, eg Bool : *{0} : *{1}):
NCO : [kind : *{1}] [lty : kind] [rty : kind] *{0}
Then, we can generalize TRANS and SYM to work on NCO: (in practice we'd
use ad-hoc polymorphism)
TRANS_n : [kind : *{1}] [t1 : kind] [t2 : kind] [t3 : kind] [lco : NCO
kind t1 t2] [rco : NCO kind t2 t3] NCO kind t1 t3
SYM_n : [kind : *{1}] [t1 : kind] [t2 : kind] [co : NCO kind t1 t2] NCO
kind t2 t1
A subtyping relation exists:
SUB : [kind : *{1}] [t1 : kind] [t2 : kind] [co : CO kind t1 t2] NCO kind
t1 t2
and REFL, CAST use NCO; while (this is very important) COMP, LEFT, and
RIGHT continue to use full CO's. Thus a NCO represents a coercion that is
only valid at the top level because it cannot be composed, and this
restriction is enforced by Core Lint. (Perhaps it would be good to make
other kinds of type function use NCO?)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1496>
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
