Can I reason by pattern matching and contradiction in type families?

Learn
1

Situation

Consider this type of heterogeneous binary trees, where I apply Maybe to every leaf:

data S a b = S a b

type family MaybeTree a where
  MaybeTree (S a b) = S (MaybeTree a) (MaybeTree b)
  MaybeTree a = Maybe a

I can calculate on the type level whether a certain type is a type of nodes or leaves:

type family Node a where
  Node (S a b) = 'True
  Node a = 'False

Problem

But I can’t figure out how to use this information:

myJust :: (Node a ~ 'False) => a -> MaybeTree a
myJust = Just
-- Could not deduce (MaybeTree a ~ Maybe a)
--  from the context: Node a ~ 'False

Basically, I would like to recurse over the two “patterns” of the type family, and derive a contradiction in the S case. Can I work around this, without changing the definition of S and MaybeTree?

What I’ve tried so far

Classes

instance (GJust a, GJust b) => GJust (S a b) where
  gJust (S a b) = S (gJust a) (gJust b)

instance GJust a where
  gJust = Just
  -- Couldn't match type: MaybeTree a
  --                with: Maybe a

Also, adding a (Composite a ~ 'False) constraint to the second instance doesn’t help.

I don’t understand why GHC doesn’t complain about overlapping instances here.

Singletons

data Sing a where
  SingS :: Sing a -> Sing b -> Sing (S a b)
  SingA :: Sing a

singJust :: Sing a -> a -> MaybeTree a
singJust (SingS sa sb) (S a b) = S (singJust sa a) (singJust sb b)
singJust SingA a = Just a

Same problem.

Classes with type family definition inside

instance (HasMaybeTree a, HasMaybeTree b) => HasMaybeTree (S a b) where
  -- error: Conflicting family instance declarations
  type MaybeTree' (S a b) = S (MaybeTree' a) (MaybeTree' b)
  hasJust (S a b) = S (hasJust a) (hasJust b)

instance HasMaybeTree a where
  type MaybeTree' a = a
  hasJust = Just
2

Maybe there is some way building up explicit dictionaries of inequality constraints somehow, and passing them around?

3

Normally, you would write your functions against the final type, not the type family one.
But as you know, you can’t because myJust doesn’t have the same type depending a.
The only way to have multiple myJust is to use some classes at some point. In that case you might be better using the type family inside the class definition (I’m not sure of the exact name).

4

That doesn’t work here unfortunately, moving the type definition inside a class leads to conflicting type family definitions. I’ve updated the question.

5

Have you tried a typeclass for myJust and instanciate them with different types of MaybeTree structure ?

6

Sorry, I misread you post.
Indeed the class with the type inside doesn’t work. It seems there is a ticke about it.
I’m not sure why not. I thought tha was the point of it.
Anyway, you can do that

class C a where
    myJust :: a ->  MaybeTree a

instance (C a, C b) => C (S a b) where
   myJust (S a b) = S (myJust a) (myJust b)
   
instance MaybeTree a ~ Maybe a =>  C a where
   myJust = Just

and can probably define a constraint Node or use some class trick using functional dependencies.