Holes should be representation-polymorphic
I often use holes while writing long expressions out in GHCi in order to let the typechecker assist me with type inference.
Sometimes though I find myself in a situation where I want to use holes near unlifted types and that results in kind check messages obscuring the holes or having hole errors not show up at all:
> I# (_ +# 1#)
<interactive>:5:5: error:
• Couldn't match a lifted type with an unlifted type
When matching the kind of ‘Int#’
• In the first argument of ‘(+#)’, namely ‘_’
In the first argument of ‘I#’, namely ‘(_ +# 1#)’
In the expression: I# (_ +# 1#)
<interactive>:5:5: error:
• Found hole: _ :: Int#
• In the first argument of ‘(+#)’, namely ‘_’
In the first argument of ‘I#’, namely ‘(_ +# 1#)’
In the expression: I# (_ +# 1#)
• Relevant bindings include it :: Int (bound at <interactive>:5:1)
(Don't be deceived, the type of _
there is actually Int# |> (TYPE U(hole:{a1qG}, 'IntRep, 'PtrRepLifted)_N)_N
)
Perhaps the type of _
should be forall r (a :: TYPE r). a
or even forall k (a :: k). a
instead?
This might lead to issues with -fdefer-typed-holes
but maybe we could at first disallow deferred unlifted-kinded holes? But in theory a hole is just a call to error
which is representation-polymorphic already.