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?

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.