Conflicting family instance declarations

[o1lo01ol1o]

I have an (internal,) inductive GADT for which I am trying to derive (or write) HasRep and TargetOb instances. Deriving HasRep fails for clear reasons, however, it's not clear how the correct instance could be written:

data Foo a where
  FooNat :: Natural -> Foo Natural
  FooIsEven :: Natural -> Foo Bool
  FooBar :: Bar a -> Foo a
  FooBaz :: Baz a -> Foo a

data Bar a where
  BarNone :: Bar Word64
  SomeBazIsTrue :: Some Baz -> Bar Bool

data Baz a where
  Inductive :: Foo a -> Baz a

deriveHasRep ''Baz
deriveHasRep ''Bar
deriveHasRep ''Foo

This generates the following Rep type instaces for Foo which obviously overlap:

Rep (Foo Bool) = Natural
Rep (Foo a) = Either (Bar a) (Baz a)

However, it seems like these mutually inductive GADTS could be encoded if there was type family dependency on Rep such that we could ensure that there is only ever one instance for each concrete type of the index plus the polymorphic (inductive) index. Maybe something like type Rep a = r | r -> a as outlined here.

Would something like this work?

[sellout]

Yeah, you’re correct that this is where the current approach breaks down. I would love to see a solution!

I don't think the fundep will help, even in that page, they indicate that you still have to manually make an instance for each concrete a. Also, in your case, you should have a third instance Rep (Foo Natural) = Natural, and that would conflict with Rep (Foo Bool) = Bool given the fundep, so it just causes more problems for you. The way to avoid it in your case is to repeat the HasRep (Foo a) instance substituting each concrete type you want to use for a, which is annoying at best, and untenable if the set of types is open.

One mitigating thing I've considered is pulling Rep out of HasRep, then making it possible to generate just HasRep methods. Then you could maybe get away with something like

deriveHasRepMethods ''Foo
type instance Rep (Foo Bool) = Natural
type instance Rep (Foo Natural) = Natural
type instance Rep (Foo Int) = Either (Bar Int) (Baz Int)
type instance Rep (Foo Word) = Either (Bar Word) (Baz Word)

It has the same fundamental problem, but reduces the manual work compared to the duplicated abst/repr methods.

As an aside, I think the docs mention this problem. Wondering if you saw the docs that discussed it, if so, whether they made sense; and if not, where you looked (if at all). This is just to help me improve our docs, certainly no disparagement of your diagnostics.

[o1lo01ol1o]

The way to avoid it in your case is to repeat the HasRep (Foo a) instance substituting each concrete type you want to use for a, which is annoying at best, and untenable if the set of types is open.

Thanks for the explanation! In my case they are finite as they're used as keys in a DSum, so this is workable if a little tedious.

It has the same fundamental problem, but reduces the manual work compared to the duplicated abst/repr methods.

This seems like an easy improvement in the current situation and, for the cases where the types of index are finite, you could traverse the tree in template Haskell to generate the needed type instances (I think).

As an aside, I think the docs mention this problem. Wondering if you saw the docs that discussed it, if so, whether they made sense; and if not, where you looked (if at all). This is just to help me improve our docs, certainly no disparagement of your diagnostics.

No worries! I also thought it was mentioned but I only found this passing comment about GADTs. Looking back, it seems like this issue should have been in categorifier and not here in the c target-category but it was part of a previous issue I raised about recursive types at the boundaries of the category, so I instinctively opened it in the same place.

[sellout]

Let me know if you have any issues with the manual implementation. I just tried separating the type family from the class and ran into some (avoidable) issues in using it the way I want. Basically, deriveHasRep assumes the GADT case types are disjoint, whereas the problem you're having crops up exactly where they're not.

Basically, where I suggested

deriveHasRepMethods ''Foo
type instance Rep (Foo Bool) = Natural
type instance Rep (Foo Natural) = Natural
type instance Rep (Foo Int) = Either (Bar Int) (Baz Int)
type instance Rep (Foo Word) = Either (Bar Word) (Baz Word)

earlier, those first two cases should actually be more like

type instance Rep (Foo Bool) = Either Natural (Either (Bar Bool) (Baz Bool))
type instance Rep (Foo Natural) = Either Natural (Either (Bar Natural) (Baz Natural))

I.e., the FooBar and FooBaz constructors can also be applied to Bool and Natural, so those instances need to cover three cases.

[sellout]

Here is the first part of the change: con-kitty/categorifier#72

The second part will add a deriveHasRepMethods splice, but the complicated part there is doing the right thing with overlapping cases. This first change at least makes the manual instances a bit less duplicate-y.

Going to write better docs around this, too, so happy for any feedback for that in the PR.

[zliu41]

Two thoughts:

• If we make categorify run in CoreM, then that would open up possibilities of using something per-GADT instead of a single HasRep and Rep for everything (e.g., HasRepFoo and RepFoo). That would allow writing RepFoo as a closed type family and avoiding specialization of type variables.
• Is it safe to define a single type instance Rep (Foo a) = Either (Either Natural Natural) (Either (Bar a) (Baz a)) using unsafeCoerce?

[zliu41]

I tried the second approach:

instance HasRep (Foo a) where
  Rep (Foo a) = Either (Either Natural Natural) (Either (Bar a) (Baz a))

  abst = \case
    FooNat nat -> unsafeCoerce (Left (Left nat))
    ...

The problem isn't unsafeCoerce, but when you have a Foo Nat, you'd get a "runtimeError @ 'LiftedRep @ Output "Impossible case alternative"#" for the FooIsEven case in Core, and I don't immediately see a good way to deal with that.

[sellout]

@zliu41 Can you explain a bit more about the first approach? I don't understand how it works.

[zliu41]

@zliu41 Can you explain a bit more about the first approach? I don't understand how it works.

Never mind, I don't think it works. I was thinking if Rep was closed then we don't need to instantiate the a:

type family Rep a where
  Rep (Foo Bool) = Either Natural (Either (Bar Bool) (Baz Bool))
  Rep (Foo Natural) = Either Natural (Either (Bar Natural) (Baz Natural))
  Rep (Foo a) = Either (Bar a) (Baz a)

but then there's no way to implement repr :: Foo a -> Rep (Foo a).

[sellout]

Ok, the linked PR should give you a pretty good situation (although it still needs to be cleaned up a lot). This should be what your code looks like now, I hope

deriveHasRep ''Baz
deriveHasRep ''Bar
deriveHasRep ''Foo

-- | Ideally this could be provided by `deriveHasRep`.
type FooRepPattern a = Either (Bar a) (Baz a)

-- The `Rep` instances for `Natural` and `Bool` are still provided by `deriveHasRep`.
type instance Rep (Foo Char) = FooRepPattern Char
type instance Rep (Foo Int64) = FooRepPattern Int64

Let me know if you try that and whether it works.

[o1lo01ol1o]

Ok, the linked PR should give you a pretty good situation (although it still needs to be cleaned up a lot). This should be what your code looks like now, I hope

deriveHasRep ''Baz
deriveHasRep ''Bar
deriveHasRep ''Foo

-- | Ideally this could be provided by `deriveHasRep`.
type FooRepPattern a = Either (Bar a) (Baz a)

-- The `Rep` instances for `Natural` and `Bool` are still provided by `deriveHasRep`.
type instance Rep (Foo Char) = FooRepPattern Char
type instance Rep (Foo Int64) = FooRepPattern Int64

Let me know if you try that and whether it works.

Thanks for the update. It looks like categorifier-c needs an update to compile with the linked PR:

Categorifier/C/CExpr/Cat.hs:890:8: error:
    Ambiguous occurrence ‘Rep’
    It could refer to
       either ‘Representable.Rep’,
              imported qualified from ‘Data.Functor.Rep’ at Categorifier/C/CExpr/Cat.hs:126:1-50
           or ‘G.Rep’,
              imported qualified from ‘GHC.Generics’ at Categorifier/C/CExpr/Cat.hs:138:1-34
    |
890 |   type Rep () = ()
    |        ^^^
cabal: Failed to build categorifier-c-0.1 

[sellout]

Sorry – got a (draft) PR up on this repo that bumps the dependency and fixes the things that break.