Muddling Constraint and * means that Core is inconsistent
I can say this:
type family F (a :: k)
type instance F (a :: Constraint) = Int
type instance F (a :: *) = Bool
This compiles to the following Core:
F :: forall (k :: BOX). k -> *
axF1 :: [a :: Constraint].F Constraint a ~ Int
axF2 :: [a :: *]. F * a ~ Bool
I can then build the following:
sym axF1[Any Constraint] ; axF2[Any *] :: Int ~ Bool
The transitivity is sound because, in Core, Constraint
and *
are indistinguishable.
I don't think there's a way to actually cause a bug in a running program due to this problem, but we should probably patch it up.
Possible resolution: Have coreView
change Constraint
to *
.
Possible resolution once we have * :: *
: Make Constraint
and *
representationally equal. In other words, it would be as if Constraint
were a newtype around *
. I haven't thought out the ramifications of this decision, but there's something nice about it.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |