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