On Sun Jun 4 12:00:21 UTC 2017, Anthony Clayden wrote:

I think this shows that using class instances to both define methods and drive selection logic can fail to separate concerns.

Richard's been (quite correctly) prodding me to explain why I want a no-instance in places, rather than an `instance ,,, fails` or `instance (TypeError ... ) => ...` I think Figure 7 in Garrett's 2015 paper provides a case in point. I find that `type family Ifi` and its call line 5/6 above to be more like an exercise in obfuscated type-programming. `type family Into` doesn't observe kind-hygiene in the way we'd expect a term-level function to observe type-hygiene. Type families `Into` or Ifi` might properly return: * Refl | L lp | R rp -- that could be a DataKind (where `lp` or `rp` is from a recursive call to `Into`) * or `Nope` -- which is a Boolean DataKind (yeuch) Yes `Into` does need to chase down the data structure in order to return the correct L/R accessor. But it doesn't need to also encode failure in that way. The frustrating thing (for me as reader) is `type family IsIn` is looking ahead inside the data structure to find `f`. Isn't that enough lookahead and error detection? I want there to be no equation for `Into` returning `Nope`. So I want no Line 7, nor line 10, 13 in `type family Ifi`. I think I'd tackle it this way. Instead of `type family IsIn` returning a Boolean,

type family CountF f g :: Nat where CountF f f = (S Z) CountF f (g :+: h) = Plus (CountF f g) (CountF f h) CountF f g = Z

Then for `Into` I'd use a count-preparing helper function, (instead of `Ifi`) and avoid those `Nope` returns:

type family Into f g where Into f f = Refl Into f (g :+: h) = IntoLR f (g :+: h) (CountF f g) (CountF f h) -- no fail case needed

type family IntoLR f g (cg :: Nat) (ch :: Nat) type instance Into' f (g :+: h) (S Z) Z = L (Into f g) type instance Into' f (g :+: h) Z (S Z) = R (Into f h) -- no fail case needed, no overlap, so not closed

So if the counts return {Z, Z} or {S Z, S Z} or {S (S (S Z)), S (S (S (S Z)))}, etc, there's simply no instance for `IntoLR`. (If you want a helpful error message, of course easy enough to add failure instances.) For completeness, I'll give the Instance Guard version for `CountF` and `Into`:

type family {-# INSTANCEGUARD #-} CountF f g :: Nat type instance CountF f f = (S Z) type instance CountF f (g :+: h) | f /~ (g :+: h) = Plus (CountF f g) (CountF f h) type instance CountF f g | f /~ g, g /~ (_ :+: _) = Z

type family {#- INSTANCEGUARD -#} Into f g type instance Into f f = Refl type instance Into f (g :+: h) | f /~ (g :+: h) = IntoLR f (g :+: h) (CountF f g) (CountF f h)

Those families/instances could be Associated types, grounded in the class instances (also guarded). Now I can see my way to translating this into Haskell 2010. AntC