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