aplikacje typu i ograniczające rodzaje

Question

(nie jestem całkowicie zaznajomiony z wewnętrznych mechanizmów przymusu Haskell jest solver więc mogłoby to prawdopodobnie kwestia rekrut.)

Gdy próbuje użyć aplikacji typu na GHC 8.0.1, jak pokazano w poniższym kodzie próbki

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, ScopedTypeVariables, TypeApplications #-} 
module Test where 

import Data.Constraint 

test0 :: forall (b :: *) . (forall a . a -> Bool) -> b -> Bool 
test0 g = g @b 

test1 :: forall (c :: * -> Constraint) (b :: *) . (c b) => (forall a . c a => a -> Bool) -> b -> Bool 
test1 g = g @b 

daje mi następujące błędy

• Could not deduce: c0 b 
    from the context: c b 
    bound by the type signature for: 
       test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool 
    at Test.hs:9:10-101 
• In the ambiguity check for ‘test1’ 
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
    In the type signature: 
    test1 :: forall (c :: * -> Constraint) (b :: *). 
      (c b) => (forall a. c a => a -> Bool) -> b -> Bool 

i

• Could not deduce: c a 
    from the context: c b 
    bound by the type signature for: 
       test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool 
    at Test.hs:9:10-101 
    or from: c0 a 
    bound by the type signature for: 
       test1 :: c0 a => a -> Bool 
    at Test.hs:9:10-101 
• In the ambiguity check for ‘test1’ 
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
    In the type signature: 
    test1 :: forall (c :: * -> Constraint) (b :: *). 
      (c b) => (forall a. c a => a -> Bool) -> b -> Bool 

test0 działa tam, gdzie nie ma żadnych ograniczeń, ale test1 nie.

Answer 1

Jeśli masz włączone TypeApplications, powinieneś również włączyć AllowAmbiguousTypes. Jeśli to zrobisz, błąd zniknie.

Obiekt odrzuca definicje t w taki sposób, że adnotacja o wartości t :: type nigdy nie sprawdzi. Na przykład:

test1 :: Show a => Int 
test1 = 0 

Jeśli staramy się wykorzystywać test1 gdzie indziej w naszym programie, możemy stwierdzić, że nie ma sposobu, aby rozwiązać Show a ograniczenie w drodze :: adnotacji. Dlatego kontrola niejednoznaczności odrzuca samą definicję.

Oczywiście przy aplikacjach typu kontrola niejednoznaczności staje się bez znaczenia (prawdopodobnie domyślnie powinna być wyłączona w tym przypadku), ponieważ test1 @type jest w porządku i jest całkowicie określona, ​​gdy dostępna jest instancja Show type.

Należy zauważyć, że nie jest to to samo, co słynna niejednoznaczność show . read. Że nadal produkuje błąd, z AllowAmbiguousTypes TOO:

test2 = show . read 
-- "ambiguous type variable prevents the constraint from being solved" 

operacyjnym wartości z c => t typów są tylko funkcje z c -typed przypadkach do t. Samo zdefiniowanie test1 jest w porządku, ponieważ zawsze możemy zdefiniować stałą funkcję. Jednak w show . read musimy dostarczyć instances jako argument (lub nie ma kodu do uruchomienia), i nie ma sposobu, aby je rozwiązać. Użycie aplikacji test1 bez aplikacji typu będzie równie niejednoznaczne.