From d4b3ade83cbdddc8ceb5ea43ee815a9b35e88170 Mon Sep 17 00:00:00 2001 From: Vilem Liepelt <17603372+buggymcbugfix@users.noreply.github.com> Date: Thu, 18 Dec 2025 19:44:41 +0100 Subject: [PATCH] wip --- frontend/src/Language/Granule/Checker/Kinding.hs | 7 ++++++- frontend/tests/cases/negative/simple/set.gr.output | 3 +++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 frontend/tests/cases/negative/simple/set.gr.output diff --git a/frontend/src/Language/Granule/Checker/Kinding.hs b/frontend/src/Language/Granule/Checker/Kinding.hs index a4ae4ed4..81c3fb91 100644 --- a/frontend/src/Language/Granule/Checker/Kinding.hs +++ b/frontend/src/Language/Granule/Checker/Kinding.hs @@ -1303,7 +1303,12 @@ requiresSolver s ty = do case result of -- Checking as coeffect or effect caused an error so ignore Left _ -> return False - Right _ -> putChecker >> return True + Right _ -> + -- avoid putting sets into the solver as the solver is weak on this + case isSet ty of + Just _ -> putChecker >> return False + Nothing -> + putChecker >> return True instance Unifiable Substitutors where unify' (SubstT t) (SubstT t') = unify' t t' diff --git a/frontend/tests/cases/negative/simple/set.gr.output b/frontend/tests/cases/negative/simple/set.gr.output new file mode 100644 index 00000000..809299fb --- /dev/null +++ b/frontend/tests/cases/negative/simple/set.gr.output @@ -0,0 +1,3 @@ +Type checking failed: +Falsifiable theorem: frontend/tests/cases/negative/simple/set.gr:14:1: + When checking `non-example`, {Contacts} is not approximatable by {Location} for type Set Privilege \ No newline at end of file