From ec5f510e521ecbb5b5473eb54f5933e8c1c65f59 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 19 Sep 2023 15:19:57 +0100 Subject: [PATCH] chore(hole/annotation elision): link to github bug tracker Signed-off-by: Ben Price --- primer/src/Primer/Typecheck.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 2f49f564e..3cf31c87f 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -803,6 +803,14 @@ check t = \case -- this can lead to the output being the same as the input, but with -- ID of the top hole changed, leading to losing cursor positions etc. -- But we do want to remove nested holes. + -- + -- TODO: There are known issues with this logic, see + -- - https://github.com/hackworthltd/primer/issues/7 + -- (the general issue) + -- - https://github.com/hackworthltd/primer/pull/1120#discussion_r1329972556 + -- (we noticed a specific strange behavior where a redundant + -- holey annotation was not elide even though it was identical to + -- the outer type information: foo : ∀a:*.? ; foo = {? ? : ∀a:*.? ?} (Hole _ e'@Hole{}, SmartHoles) -> check t e' -- we strip off one layer, and hit this case again. (Hole _ (Ann _ e' TEmptyHole{}), SmartHoles) ->