search

IaFP / ghc

A slightly more Glorious Haskell Compiler
Other
2 stars 0 forks source link

Injective Open Type families #20

Closed fxdpntthm closed 2 years ago

fxdpntthm commented 2 years ago

Consider 

data GenLocated l e = L l e
type family Anno a b = b
-- type family $wf'Anno a b

type family XRec p a = r | r -> a
-- type family $wf'XRec p a = r | r -> a

type instance XRec (GhcPass p) a = GenLocated (Anno a) a
-- $wf'XRec (GhcPass p) a = (GenLocated @ Anno a, GenLocated (Anno a) @ a, $wf'Anno a)

gives an error:

   Type family equation violates the family's injectivity annotation.
    Type variable ‘a’ cannot be inferred from the right-hand side.
    In the type family equation:
      $wf'XRec (GhcPass p) a = (GenLocated @ Anno a,
                                GenLocated (Anno a) @ a, $wf'Anno a)
        -- Defined at compiler/GHC/Hs/Extension.hs:100:15

I think the issue is that (GenLocated @ Anno a, GenLocated (Anno a) @ a) should just reduce to () giving us:

$wf'XRec (GhcPass p) a ~ $wf'Anno a

Also should mirror WF TFs really be injective?