Promoting newtype destructor
given
newtype LOL a = MkLOL { unLOL :: [[a]] }
I'd like to write
type family UnLOL (lol :: LOL a) = (result :: [[a]]) | result -> lol
type instance UnLOL ('MkLOL xss) = xss
This is currently not accepted, but AFAICS it should be injective, as lol
is kind restricted. Especially the example in injective type families paper do not apply, as UnLOL Int
is ill-kinded.
With this GHC could infer lol ~ MkLOL xss
from UnLOL lol ~ xss
, so newtypes would be useful for type-level programming, as type (kind) synonyms cannot be partially applied.
Trac metadata
Trac field | Value |
---|---|
Version | |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire, kosmikus |
Operating system | |
Architecture |