Fix examples/set.gr

Author: buggymcbugfix

examples/set.gr

@@ -16,8 +16,4 @@ example =
       [contacts] : (List String) [{Contacts}] = getContacts
   in [Cons location contacts]
 
-non-example : (List String) [{Contacts}]
-non-example =
-  let [location] : String [{Location}] = getLocation;
-      [contacts] : (List String) [{Contacts}] = getContacts
-  in [Cons location contacts]
+-- see frontend/tests/cases/negative/simple/set.gr for a failing example

frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs

@@ -11,10 +11,11 @@ import Language.Granule.Checker.Constraints.SynTree
 import Language.Granule.Syntax.Type
 
 import GHC.Generics (Generic)
+import GHC.Stack (HasCallStack)
 import Data.SBV hiding (kindOf, name, symbolic)
 import qualified Data.SBV.Set as S
 
-solverError :: String -> a
+solverError :: HasCallStack => String -> a
 solverError = error
 
 -- Symbolic grades, for coeffects and indices

frontend/src/Language/Granule/Checker/Kinding.hs

@@ -317,6 +317,14 @@ synthKindWithConfiguration s config (TyApp (TyCon (internalName -> "Set")) t) =
     -- otherwise kind of the set depends on the kind of the elements
     k      -> return (k, subst, TyApp (TyCon (mkId "Set")) t')
 
+synthKindWithConfiguration s config (TyApp (TyCon (internalName -> "SetOp")) t) = do
+  (k, subst, t') <- synthKindWithConfiguration s config t
+  case k of
+    -- For set over type, default to the kind being Effect
+    Type 0 -> return (keffect, subst, TyApp (TyCon (mkId "SetOp")) t')
+    -- otherwise kind of the set depends on the kind of the elements
+    k      -> return (k, subst, TyApp (TyCon (mkId "SetOp")) t')
+
 -- KChkS_app
 --
 --      t1 => k1 -> k2    t2 <= k1
@@ -1298,9 +1306,9 @@ requiresSolver s ty = do
     Right _ ->
       -- avoid putting sets into the solver as the solver is weak on this
       -- TODO: consider something better here
-      case isSet ty of
-       Just _ ->  putChecker >> return False
-       Nothing ->
+      -- case isSet ty of
+      --  Just _ ->  putChecker >> return False
+      --  Nothing ->
         putChecker >> return True
 
 instance Unifiable Substitutors where

frontend/tests/cases/negative/simple/set.gr

@@ -0,0 +1,17 @@
+language GradedBase
+
+data List a = Cons a (List a) | Nil
+
+data Privilege = Camera | Contacts | Location | Microphone
+
+getLocation : String [{Location}]
+getLocation = ["051.28°N 001.08°E"]
+
+getContacts : (List String) [{Contacts}]
+getContacts = [Cons "Alice" (Cons "Bob" (Cons "Carol" Nil))]
+
+non-example : (List String) [{Contacts}]
+non-example =
+  let [location] : String [{Location}] = getLocation;
+      [contacts] : (List String) [{Contacts}] = getContacts
+  in [Cons location contacts]