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