Błędna rozdzielczość typu otworu

Niedawno odkryłem, że dziury typu połączone z dopasowywaniem wzorców na próbach zapewniają całkiem przyjemne doświadczenie w stylu Agdy w Haskell. Na przykład:

{-# LANGUAGE
    DataKinds, PolyKinds, TypeFamilies, 
    UndecidableInstances, GADTs, TypeOperators #-}

data (==) :: k -> k -> * where
    Refl :: x == x

sym :: a == b -> b == a
sym Refl = Refl 

data Nat = Zero | Succ Nat

data SNat :: Nat -> * where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

type family a + b where
    Zero   + b = b
    Succ a + b = Succ (a + b)

addAssoc :: SNat a -> SNat b -> SNat c -> (a + (b + c)) == ((a + b) + c)
addAssoc SZero b c = Refl
addAssoc (SSucc a) b c = case addAssoc a b c of Refl -> Refl

addComm :: SNat a -> SNat b -> (a + b) == (b + a)
addComm SZero SZero = Refl
addComm (SSucc a) SZero = case addComm a SZero of Refl -> Refl
addComm SZero (SSucc b) = case addComm SZero b of Refl -> Refl
addComm sa@(SSucc a) sb@(SSucc b) =
    case addComm a sb of
        Refl -> case addComm b sa of
            Refl -> case addComm a b of
                Refl -> Refl 

Naprawdę fajną rzeczą jest to, że mogę zastąpić prawe strony Refl -> expkonstrukcji otworem typu, a moje typy celów do otworów są aktualizowane o dowód, prawie tak jak w przypadku rewriteformularza w Agdzie.

Jednak czasami dziura po prostu nie aktualizuje się:

(+.) :: SNat a -> SNat b -> SNat (a + b)
SZero   +. b = b
SSucc a +. b = SSucc (a +. b)
infixl 5 +.

type family a * b where
    Zero   * b = Zero
    Succ a * b = b + (a * b)

(*.) :: SNat a -> SNat b -> SNat (a * b)
SZero   *. b = SZero
SSucc a *. b = b +. (a *. b)
infixl 6 *.

mulDistL :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL SZero b c = Refl
mulDistL (SSucc a) b c = 
    case sym $ addAssoc b (a *. b) (c +. a *. c) of
        -- At this point the target type is
        -- ((b + c) + (n * (b + c))) == (b + ((n * b) + (c + (n * c))))
        -- The next step would be to update the RHS of the equivalence:
        Refl -> case addAssoc (a *. b) c (a *. c) of
            Refl -> _ -- but the type of this hole remains unchanged...

Ponadto, nawet jeśli typy docelowe niekoniecznie są wyrównane w dowodzie, jeśli wkleię całość z Agdy, nadal sprawdza się dobrze:

mulDistL' :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL' SZero b c = Refl
mulDistL' (SSucc a) b c = case
    (sym $ addAssoc b (a *. b) (c +. a *. c),
    addAssoc (a *. b) c (a *. c),
    addComm (a *. b) c,
    sym $ addAssoc c (a *. b) (a *. c),
    addAssoc b c (a *. b +. a *. c),
    mulDistL' a b c
    ) of (Refl, Refl, Refl, Refl, Refl, Refl) -> Refl

Czy masz jakieś pomysły, dlaczego tak się dzieje (lub jak mogę zrobić poprawną korektę dowodu w solidny sposób)?

Jeśli chcesz wygenerować wszystkie możliwe takie wartości, możesz napisać funkcję, która to zrobi, z podanymi lub określonymi granicami.

Może być całkiem możliwe użycie cyfr kościelnych na poziomie typu lub innych, aby wymusić ich tworzenie, ale jest to prawie zdecydowanie za dużo pracy, jak na to, czego prawdopodobnie chcesz / potrzebujesz.

To może nie być to, czego chcesz (np. „Z wyjątkiem używania tylko (x, y), ponieważ z = 5 - x - y”), ale ma to większy sens niż próba wprowadzenia pewnego rodzaju wymuszonego ograniczenia na poziomie typu, aby umożliwić prawidłowe wartości.

Dzieje się tak, ponieważ wartości są określane w czasie wykonywania. Może spowodować transformację wartości w zależności od tego, co zostało wprowadzone w czasie wykonywania, dlatego zakłada, że ​​otwór jest już zaktualizowany.