Closed
Description
@masaeedu points out:
{-# LANGUAGE DataKinds, GADTs #-}
data Z ab where
Z :: (a -> b) -> Z '(a, b)
test :: Z ab
test = _
produces
test = Z id
But it doesn't typecheck.
What's going wrong here? When we introduce the Z
constructor, we should generate two new skolems a
and b
such that '(a, b) ~ ab
. But instead we generate two new unification variables, which are thus free to unify with one another, and thus produce the bogus id
.