Techniki śledzenia ograniczeń

Oto scenariusz: napisałem trochę kodu z podpisem typu, a skargi GHC nie mogły wydedukować x ~ y dla niektórych xi y. Zwykle możesz rzucić GHC kość i po prostu dodać izomorfizm do ograniczeń funkcji, ale jest to zły pomysł z kilku powodów:

1. Nie podkreśla zrozumienia kodu.
2. Możesz skończyć z 5 ograniczeniami, w których wystarczyłoby (na przykład, jeśli 5 jest implikowanych przez jedno bardziej szczegółowe ograniczenie)
3. Możesz skończyć z fałszywymi ograniczeniami, jeśli zrobiłeś coś złego lub jeśli GHC jest nieprzydatny

Właśnie spędziłem kilka godzin walcząc ze sprawą 3. Bawię się syntactic-2.0i próbowałem zdefiniować wersję niezależną od domeny share, podobną do wersji zdefiniowanej w NanoFeldspar.hs.

Miałem to:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

i GHC could not deduce (Internal a) ~ (Internal b), co z pewnością nie było tym, do czego dążyłem. Więc albo napisałem kod, którego nie zamierzałem (co wymagało ograniczenia), albo GHC chciało tego ograniczenia z powodu innych ograniczeń, które napisałem.

Okazuje się, że musiałem dodać (Syntactic a, Syntactic b, Syntactic (a->b))do listy ograniczeń, z których żaden nie sugeruje (Internal a) ~ (Internal b). Zasadniczo natknąłem się na właściwe ograniczenia; Nadal nie mam systematycznego sposobu na ich znalezienie.

Moje pytania to:

1. Dlaczego GHC zaproponowało to ograniczenie? Nigdzie w składni nie ma ograniczenia Internal a ~ Internal b, więc skąd GHC to wzięło?
2. Zasadniczo, jakich technik można użyć do prześledzenia źródła ograniczenia, które według GHC jest potrzebne? Nawet dla ograniczeń, że można dowiedzieć się, moje podejście jest zasadniczo brute zmusza ścieżkę przestępstwa przez fizycznie spisując cyklicznych ograniczeń. To podejście polega zasadniczo na zejściu nieskończonej króliczej dziury ograniczeń i dotyczy mniej efektywnej metody, jaką mogę sobie wyobrazić.

Po pierwsze, twoja funkcja ma zły typ; Jestem pewien, że tak powinno być (bez kontekstu) a -> (a -> b) -> b. GHC 7.10 jest nieco bardziej pomocny w zaznaczeniu tego, ponieważ w twoim oryginalnym kodzie narzeka na brakujące ograniczenie Internal (a -> b) ~ (Internal a -> Internal a). Po naprawieniu sharetypu GHC 7.10 pozostaje pomocny w prowadzeniu nas:

1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

2. Po dodaniu powyższego otrzymujemy Could not deduce (sup ~ Domain (a -> b))

3. Po dodaniu, że możemy dostać Could not deduce (Syntactic a), Could not deduce (Syntactic b)aCould not deduce (Syntactic (a -> b))

4. Po dodaniu tych trzech ostatecznie sprawdza typ; więc kończymy

   share :: (Let :<: sup,
             Domain a ~ sup,
             Domain b ~ sup,
             Domain (a -> b) ~ sup,
             Internal (a -> b) ~ (Internal a -> Internal b),
             Syntactic a, Syntactic b, Syntactic (a -> b),
             SyntacticN (a -> (a -> b) -> b) fi)
         => a -> (a -> b) -> b
   share = sugarSym Let
   

Więc powiedziałbym, że GHC nie był bezużyteczny w prowadzeniu nas.

Jeśli chodzi o pytanie dotyczące śledzenia, skąd GHC pobiera wymagania dotyczące ograniczenia, możesz w szczególności wypróbować flagi debugowania GHC-ddump-tc-trace , a następnie przeczytać wynikowy dziennik, aby zobaczyć, gdzie Internal (a -> b) ~ ti (Internal a -> Internal a) ~ tsą dodane do Wantedzestawu, ale będzie to dość długi odczyt .

Czy próbowałeś tego w GHC 8.8+?

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi,
          _) 
      => a -> (a -> b) -> a
share = sugarSym Let

Kluczem jest użycie dziury typu między ograniczeniami: _ => your difficult type