Thông tin chi tiết về nitty-gritty được đề cập trong các giấy tờ từ Simon Peyton-Jones, mặc dù phải mất rất nhiều chuyên môn kỹ thuật để hiểu chúng. Nếu bạn muốn đọc một bài báo về cách hoạt động của suy luận kiểu Haskell, bạn nên đọc về các kiểu dữ liệu đại số tổng quát (GADT), kết hợp các kiểu tồn tại với một số tính năng khác. Tôi đề nghị "Suy luận kiểu đầy đủ và quyết định cho GADT", trên danh sách các giấy tờ tại http://research.microsoft.com/en-us/people/simonpj/.
Định lượng hiện thực thực sự hoạt động rất giống với định lượng phổ dụng. Đây là một ví dụ để làm nổi bật các điểm tương đồng giữa hai. Chức năng useExis là vô dụng, nhưng nó vẫn là mã hợp lệ.
data Univ a = Univ a
data Exis = forall a. Exis a
toUniv :: a -> Univ a
toUniv = Univ
toExis :: a -> Exis
toExis = Exis
useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x
useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x
Trước tiên, lưu ý rằng toUniv và toExis gần như giống nhau. Cả hai đều có tham số kiểu miễn phí a vì cả hai nhà xây dựng dữ liệu đều có tính đa hình. Tuy nhiên, trong khi a xuất hiện trong loại trả lại là toUniv, nó không xuất hiện trong loại trả lại là toExis. Khi nói đến loại lỗi mà bạn có thể nhận được từ việc sử dụng một hàm tạo dữ liệu, không có sự khác biệt lớn giữa các kiểu tồn tại và phổ quát.
Thứ hai, lưu ý loại xếp hạng 2 forall a. a -> b trong useExis. Đây là sự khác biệt lớn trong suy luận kiểu. Kiểu tồn tại được lấy từ mẫu phù hợp (Exis x) hoạt động như một biến kiểu bổ sung, ẩn được chuyển đến phần thân của hàm, và nó không được thống nhất với các kiểu khác. Để làm cho điều này rõ ràng hơn, đây là một số khai báo sai của hai hàm cuối cùng mà chúng ta cố gắng hợp nhất các kiểu không được thống nhất. Trong cả hai trường hợp, chúng tôi buộc loại x được hợp nhất với biến loại không liên quan. Trong useUniv, biến kiểu là một phần của kiểu hàm. Trong useExis, đó là loại tồn tại từ cấu trúc dữ liệu.
useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
-- Variable 'a' is there in the function type
useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
-- Variable 'a' comes from the pattern "Exis x",
-- via the existential in "data Exis = forall a. Exis a".