Lỗi loại khi gán một loại forall hợp lệ vào biến giới hạn

Question

Đây có phải là lỗi trong trình kiểm tra loại không?

Prelude> let (x :: forall a. a -> a) = id in x 3 

<interactive>:0:31: 
    Couldn't match expected type `forall a. a -> a' 
       with actual type `a0 -> a0' 
    In the expression: id 
    In a pattern binding: (x :: forall a. a -> a) = id 

Thực tế là không ở trên để gõ kiểm tra, nhưng sự nhăn mặt này thành công:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id 
3 

dẫn tôi nghĩ rằng "chuyển đổi prenex yếu" (xem trang 23 của this paper) có thể liên quan bằng cách nào đó . Nhúng một forall vào một vị trí contravariant nơi nó không thể "trôi nổi" dường như giữ nó an toàn khỏi lỗi kỳ lạ này.

Answer 1

Điều tôi nghĩ đang xảy ra ở đây là: Trong tiêu chuẩn Damas – Suy luận kiểu Milner, hãy ràng buộc là nơi duy nhất để khái quát hóa một loại xảy ra. Chữ ký kiểu mà ví dụ không sử dụng của bạn là pattern type signature mà "hạn chế loại mẫu theo cách hiển nhiên". Bây giờ, trong ví dụ này, nó không phải là "rõ ràng" cho dù ràng buộc này nên xảy ra trước hoặc sau khi tổng quát, nhưng ví dụ thất bại của bạn chứng minh, tôi nghĩ rằng, nó được áp dụng trước khi tổng quát hóa.

Đặt cụ thể hơn: trong một let ràng buộc let x = id in ..., những gì xảy ra là id 's loại forall a. a->a được instantiated thành một giống duy nhứt, nói a0 -> a0, sau đó được bổ nhiệm làm x' loại s và sau đó được khái quát hóa như forall a0. a0 -> a0. Nếu, như tôi nghĩ, chữ ký kiểu mẫu được kiểm tra trước khi khái quát hóa, về cơ bản nó yêu cầu trình biên dịch xác minh rằng kiểu đơn a0 -> a0 là tổng quát hơn so với polytype forall a. a -> a, mà nó không phải là.

Nếu chúng ta di chuyển chữ ký loại đến mức ràng buộc, let x :: forall a. a-> a; x = id in ... chữ ký được kiểm tra sau khi tổng quát (vì điều này được cho phép rõ ràng để kích hoạt đệ quy đa hình) và không xảy ra lỗi kiểu.

Cho dù đó có phải là lỗi hay không, tôi nghĩ, một vấn đề quan điểm. Có vẻ như không phải là một thông số thực tế mà sẽ cho chúng tôi biết những hành vi đúng ở đây là gì; chỉ có những kỳ vọng của chúng tôi. Tôi sẽ đề nghị thảo luận vấn đề với những người GHC.

Answer 2

Không phải là câu trả lời thực sự, nhưng quá dài để nhận xét:
Nó cũng có thể là một lỗi. Phát xung quanh một chút với biểu thức, không đáng ngạc nhiên là

hoạt động nếu viết khắc phục rõ ràng được bật. Mặc dù vậy, đó là loại 1 cấp bậc chuẩn. Một số biến thể khác:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 
3 

Được rồi, điều đó có hiệu quả, tôi không biết tại sao lambda hoạt động khác nhau, nhưng thực tế. Tuy nhiên:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 

<interactive>:0:31: 
    Couldn't match expected type `t0 -> t1' 
       with actual type `forall a. a -> a' 
    The lambda expression `\ y -> id y' has one argument, 
    but its type `forall a. a -> a' has none 
    In the expression: \ y -> id y 
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y 

(7.2.2; 7.0.4 cho cùng một lỗi). Điều đó thật đáng ngạc nhiên.