From 7cfe2e43e117861f0ba0d53768aa1f8c653ff017 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 18 Aug 2023 00:01:58 +0100 Subject: [PATCH] somewhat unrelated TODO: revisit comparing kinds up to holes Signed-off-by: Ben Price --- primer/src/Primer/Typecheck.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index e1f3ac091..2100ed882 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -980,6 +980,10 @@ consistentTypes x y = uncurry eqType $ holepunch x y 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? + -- TODO: this needs revisiting, as we can now write + -- foo : ∀a:*.? ; foo = ? : ∀a:?.? + -- and SH puts the def into a hole, as the kinds on the foralls do not exactly match. + -- I'm not yet sure what the right thing to do is, I need to think about the metatheory! (TForall () n k hs, TForall () m l ht) holepunch s t = (s, t)