Jaka jest przyczyna tego tajemniczego błędu typu Haskell polegającego na odbiciu?

Question

Grałem z pakietem Haskell reflection i napotkałem błąd typu, którego nie rozumiem w pełni. Najpierw próbowałem napisać następującą funkcję, która szczęśliwie typechecks:

{-# LANGUAGE TypeApplications #-} 

reifyGood :: (forall s. Reifies s a => Proxy a) ->() 
reifyGood p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

Co ciekawe, to jednak nieco inny program robi nie typecheck:

reifyBad :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

• Could not deduce (Reifies s s) arising from a use of ‘p’ 
    from the context: Reifies s a0 
    bound by a type expected by the context: 
       Reifies s a0 => Proxy s ->() 
• In the first argument of ‘seq’, namely ‘p @t’ 
    In the expression: p @t `seq`() 
    In the second argument of ‘reify’, namely 
    ‘(\ (_ :: Proxy t) -> p @t `seq`())’ 

wyrażenia są identyczne, ale zauważ różnicę między sygnaturami typu:

reifyGood :: (forall s. Reifies s a => Proxy a) ->() 
reifyBad :: (forall s. Reifies s s => Proxy s) ->() 

Uważam to za ciekawe. Na pierwszy rzut oka jest to nieważne, ponieważ w drugim przykładzie skolem s wymknie się spod jego zakresu. Jednakże, nie jest to faktycznie prawda, komunikat o błędzie nie wspomina Skolem ucieczki, w przeciwieństwie do tego nieco inny program:

reifyBad' :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq`() 

• Couldn't match expected type ‘t0’ with actual type ‘Proxy s’ 
    because type variable ‘s’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     Reifies s a0 => Proxy s -> t0 
• In the expression: p @t 
    In the second argument of ‘reify’, namely 
    ‘(\ (_ :: Proxy t) -> p @t)’ 
    In the first argument of ‘seq’, namely 
    ‘reify undefined (\ (_ :: Proxy t) -> p @t)’ 

Więc może coś innego jest tutaj w grę.

Badania typu reify, staje się mało jasne, że coś jest nie w porządku:

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r 

Zakresy a i s są wyraźnie różne, więc wydaje się mieć sens, że GHC nie pozwoli im ujednolicić. Jednak wydaje się, że coś z lokalnego ograniczenia równości wprowadzonego przez funkcjonalną zależność od Reifies powoduje dziwne zachowanie. Co ciekawe, ta para funkcji typechecks:

foo :: forall a r. Proxy a -> (forall s. (s ~ a) => Proxy s -> r) -> r 
foo _ f = f Proxy 

bar :: (forall a. Proxy a) ->() 
bar p = let p' = p in foo p' (\(_ :: Proxy s) -> (p' :: Proxy s) `seq`()) 

... ale usunięcie ograniczenia równości w podpisie typu foo czyni je nie typecheck, produkując błąd Skolem ucieczki:

• Couldn't match type ‘a0’ with ‘s’ 
    because type variable ‘s’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     Proxy s ->() 
    Expected type: Proxy s 
    Actual type: Proxy a0 
• In the first argument of ‘seq’, namely ‘(p' :: Proxy s)’ 
    In the expression: (p' :: Proxy s) `seq`() 
    In the second argument of ‘foo’, namely 
    ‘(\ (_ :: Proxy s) -> (p' :: Proxy s) `seq`())’ 

W tym momencie, Jestem zakłopotany. Mam kilka (bardzo powiązanych) pytań.

1. Dlaczego reifyBad nie sprawdza się najpierw przy typie?

2. Dokładniej, dlaczego powoduje wystąpienie błędu braku instancji ?

Co więcej, czy to zachowanie jest oczekiwane i dobrze zdefiniowane, czy też jest to tylko dziwny przypadek, gdy typechecker ma taki wynik?

Answer 1

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r 

wymaganiem jest to, że stanowi zasadniczo Skolem r w rodzaju powyżej nie może zależeć od s który jest ilościowo drugiego argumentu. W przeciwnym razie "uciekłoby" z jego zakresu od reify zwraca r.

W

reifyBad :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

widzimy, że drugi argument reify jest \(_ :: Proxy t) -> p @t `seq`(), więc typ r byłby typ zwracany tej funkcji, która jest (). Od r ~() nie zależy od s, tutaj nie ma problemu ucieczki.

Jednak p @t zgodnie z typem p wymaga Reifies t t. Od reify wybierze t ~ s, ograniczenie jest takie samo jak Reifies s s. Zamiast tego reify zapewnia tylko Reifies s a, gdzie a jest typu undefined.

Subtelna Chodzi o to, że podczas gdy undefined może produkować każdy rodzaj a, kontrolujący typu nie można ujednolicić s i a. Dzieje się tak dlatego, że funkcja o tym samym typie co reify jest uprawniona do otrzymania tylko jednej wartości sztywnego typu (sztywnego) a, a następnie wybierz dowolną liczbę typów zgodnie z wymaganiami. Ujednolicenie wszystkich takich s s jednym pojedynczym a byłoby błędem, skutecznie ograniczając wybór s przez reify.

Zamiast tego, w wariancie

reifyBad' :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq`() 

tutaj r wnioskuje się być typem powrotu \(_ :: Proxy t) -> p @t, który jest Proxy t, gdzie t ~ s. Ponieważ r ~ Proxy s zależy od s, wywołujemy błąd skolem.