Should consistentTypes compare kinds up to holes?

[brprice]

For reference in the sequel, consider the following two snippets:

Firstly, how we typecheck an embedding of a synthesisable term in a checkable position

e ∈ t'   t ~ t'
---------------
    t ∋ e

primer/primer/src/Primer/Typecheck.hs

Lines 794 to 799 in 1ab647e

	(t', e') <- synth e
	if consistentTypes t t'
	then pure $ addChkMetaT t e'
	else case sh of
	NoSmartHoles -> throwError' (InconsistentTypes t t')
	SmartHoles -> enholeT t e'

(ignore the fact that smartholes may transform e into e' for our current purposes)

The definition of t ~ t'

primer/primer/src/Primer/Typecheck.hs

Lines 956 to 980 in 1ab647e

	-- | Two types are consistent if they are equal (up to IDs and alpha) when we
	-- also count holes as being equal to anything.
	consistentTypes :: Type -> Type -> Bool
	consistentTypes x y = uncurry eqType $ holepunch x y
	where
	-- We punch holes in each type so they "match" in the sense that
	-- they have holes in the same places. (At least, until we find
	-- obviously different constructors.)
	holepunch (TEmptyHole _) _ = (TEmptyHole (), TEmptyHole ())
	holepunch _ (TEmptyHole _) = (TEmptyHole (), TEmptyHole ())
	holepunch (THole _ _) _ = (TEmptyHole (), TEmptyHole ())
	holepunch _ (THole _ _) = (TEmptyHole (), TEmptyHole ())
	holepunch (TFun _ s t) (TFun _ s' t') =
	let (hs, hs') = holepunch s s'
	(ht, ht') = holepunch t t'
	in (TFun () hs ht, TFun () hs' ht')
	holepunch (TApp _ s t) (TApp _ s' t') =
	let (hs, hs') = holepunch s s'
	(ht, ht') = holepunch t t'
	in (TApp () hs ht, TApp () hs' ht')
	holepunch (TForall _ n k s) (TForall _ m l t) =
	let (hs, ht) = holepunch s t
	in -- Perhaps we need to compare the kinds up to holes also?
	(TForall () n k hs, TForall () m l ht)
	holepunch s t = (s, t)

---

Now consider the definition

foo : ∀a:* . ?
foo = ? : ∀b:* . ?

which is creatable by

• in type, insert a forall which automatically writes * for the kind
• in term, create an annotation and then a forall

What should happen if we change the kind of b to a hole?
Currently this creates a term which is not type-correct, so smartholes kicks in and gives

foo : ∀a:* . ?
foo = {? ? : ∀b:? . ? ?}

but perhaps it would be more intuitive and more consistent to consider these two annotations consistent, giving

foo : ∀a:* . ?
foo = ? : ∀b:? . ?

Note that one level down we have that the following is type-correct (with no non-empty holes!)

bar : Int ->  ?
bar = ? : ? -> ?

---

Whilst I think that this would be straightforward to implement, and it seems like it would be a good idea, I have not thought about it enough to convince myself that there are no lurking pitfalls.

[georgefst]

I'd say it's not obvious where the mismatch stems from, so this sounds like something we should do (unless of course we get rid of KHole completely - discussed as unlikely recently in #1095 (comment), but I note that #108 is still open).