Overlapping families (specificity/degrees of freedom)

[Gabor Greif]

Hi Richard,

I have a question regarding type families with overlapping syntax.

In below example the last two lines are overlapped, so the first gets selected
when I present type equality witness to GHC:

> help :: Sing (ls :: Inventory a) -> Sing (r :: Inventory a) -> Sing (l :: a) -> Sing (InterAppend ls r l)
> help l@(Snoc _ _) (Snoc _ r) one | Just Eq <- isSame r one = Snoc l one    --- OKAY

> type family InterAppend (l' :: Inventory a) (r' :: Inventory a) (one' :: a) :: Inventory a
> type instance where
>   InterAppend Empty r one = Empty
>   InterAppend (More ls l) Empty one = Empty
>   InterAppend (More ls l) (More rs one) one = More (More ls l) one   --- 4 degrees of freedom
>   InterAppend (More ls l) (More rs r) one = More ls l     --- 5 degrees of freedom

However I cannot manage to trigger the last line when *not* presenting
the witness, e.g. in this case:

> help l@(Snoc _ _) (Snoc _ _) _ = l    --- DOES NOT WORK

IIRC, when implementing something like this in Omega, the type
function evaluator considered the number of type variables and tried
to match the more constrained leg (i.e. preferred less degrees of
freedom).

Can you give me a hint how this is supposed to work in your implementation?

Must I present a type non-equality witness to trigger the fourth leg
of InterAppend above?

What I am trying to implement is an intersection algorithm for
singleton-typed list witnesses,
roughly

> intersect :: SingEqual (t :: a) => Sing (lhs :: '[a]) -> Sing (rhs :: '[a]) -> Sing (Intersect lhs rhs)

... but I am not there yet, obviously!

I'd be grateful for any hint,

cheers,

    Gabor