Convince GHC that type family declarations are not overlapping

Question

So I would like to implement a function that applies a value to the nth argument of a function, lets call it inject:

inject :: (???) => a -> f -> ???

So I declared a class representing all Applicable triples (n, a, f). Note that n must be bigger than 0 and a depends on f and n

class (1 <= n) => Applicable n a f | f n -> a where
  type ApplyAt n a f :: Type
  inject :: a -> f -> ApplyAt n a f

We can then do some induction on n:

instance Applicable 1 a (a -> b) where
  type ApplyAt 1 a (a -> b) = b
  inject a f = f a

instance (Applicable (n - 1) a c) => Applicable n (a :: Type) (b -> c) where
  type ApplyAt n a (b -> c) = b -> ApplyAt (n - 1) a c
  inject a f = \x -> inject @(n - 1) a (f x)

Applicable n a (b -> c) implies Applicable (n - 1) a c which implies n - 1 >= 1 or n >= 2 so these instance declarations are not overlapping. But GHC proceeds to complain:

Conflicting family instance declarations:
  ApplyAt 1 a (a -> b) = b
  ApplyAt n a (b -> c) = b -> ApplyAt (n - 1) a c

What should I do to convince GHC that these type familiy declarations are not overlapping?

Does it work if you define your own `data N = One | Succ N` and use that instead of `GHC.TypeLits`/`GHC.TypeNats`? — Joseph Sible-Reinstate Monica, May 02 '20 at 04:39
Or this? [Haskell overlapping instances and type functions](https://stackoverflow.com/q/4463154/7509065) — Joseph Sible-Reinstate Monica, May 02 '20 at 05:02
Another related question: [Why context is not considered when selecting typeclass instance in Haskell?](https://stackoverflow.com/questions/26885067/why-context-is-not-considered-when-selecting-typeclass-instance-in-haskell) — Poscat, May 04 '20 at 11:00

Poscat · Accepted Answer · 2020-05-04T15:24:46.933

The solution is to use inductively defined natural numbers/positive integers which avoids overlapping instances.

data NPlus = One | Suc NPlus

class Applicable (n :: NPlus) a f | f n -> a where
  type ApplyAt n a f :: Type
  inject :: a -> f -> ApplyAt n a f

instance Applicable One a (a -> b) where
  type ApplyAt One a (a -> b) = b
  inject a f = f a

instance (Applicable n a c) => Applicable (Suc n) (a :: Type) (b -> c) where
  type ApplyAt (Suc n) a (b -> c) = b -> ApplyAt n a c
  inject a f = \x -> inject @n a (f x)

-- >>> inject @(Suc One) 1 (\y x -> (y + 3) * x) 2
-- 5
--

Convince GHC that type family declarations are not overlapping

1 Answers1