haskell
Improve "unification involving polytypes" message
As pointed out here, attempting to unify a metavariable with a polytype can lead to rather confusing error messages, which often mention type variables which are nowhere to be seen in the user's program:
{-# LANGUAGE RankNTypes, DataKinds #-}
import Data.Kind
type D :: forall (a :: Bool) -> Type
data D a = MkD
type E = D
* Expected kind `k0', but `D' has kind `forall (a :: Bool) -> *'
Cannot instantiate unification variable `k0'
with a kind involving polytypes: forall (a :: Bool) -> *
It would be nice to augment the error message with some more helpful information, perhaps asking the user to add more arguments, as the following is OK:
type E a = D a
Maybe @goldfirere has some suggestion about possible improvements?
As a quick improvement to this, we could check when formatting the error message whether the variable trying to be unified with a polytype is just a bare metavariable (like k0). In that case, perhaps saying
* Cannot infer polymorphic kind `forall (a :: Bool) -> *`
would be an improvement. (The use of "kind" vs "type" there is informed by existing logic, I believe.)
Such a small fix might go a long way.
A more elaborate fix would allow e.g. GHC to infer the kind of the right-hand side of a type synonym and then use that as the kind of the left-hand side. This doesn't work in recursive scenarios, but the vast majority of type synonyms are not recursive. (Type synonyms can never be recursive with themselves or other type synonyms, but a type synonym can be mutually recursive with a datatype definition.) GHC already has special treatment like this at the term level. But this is meant to be only about error messages, so I'll stop this digression here.
Hm. Evidently GitHub interprets "shift+enter" as a request to close an issue. :(