Switch around who gets to be the "Normal" Set

examples/set.gr

@@ -0,0 +1,23 @@
+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))]
+
+example : (List String) [{Contacts, Location}]
+example =
+  let [location] : String [{Location}] = getLocation;
+      [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]

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

@@ -258,7 +258,7 @@ freshSolverVarScoped quant name (isExt -> Just t) q k =
 freshSolverVarScoped quant name (TyVar v) q k =
   quant q name (\solverVar -> k (sTrue, SUnknown $ SynLeaf $ Just solverVar))
 
-freshSolverVarScoped quant name (Language.Granule.Syntax.Type.isSet -> Just (elemTy, polarity)) q k =
+freshSolverVarScoped quant name (isSet -> Just (elemTy, polarity)) q k =
       quant q name (\solverVar -> k (inUniverse solverVar, SSet polarity solverVar))
     where
 
@@ -458,8 +458,8 @@ compileCoeffect (TyGrade k' n) k _ | k == extendedNat && (k' == Nothing || k' ==
 compileCoeffect (TyRational r) (TyCon k) _ | internalName k == "Q" =
   return (SFloat  . fromRational $ r, sTrue)
 
-compileCoeffect (TySet _ xs) (Language.Granule.Syntax.Type.isSet -> Just (elemTy, polarity)) _ =
-    return ((SSet polarity) . S.fromList $ mapMaybe justTyConNames xs, sTrue)
+compileCoeffect (TySet _ xs) (isSet -> Just (elemTy, polarity)) _ =
+    return (SSet polarity . S.fromList $ mapMaybe justTyConNames xs, sTrue)
   where
     justTyConNames (TyCon x) = Just (internalName x)
     justTyConNames t = error $ "Cannot have a type " ++ show t ++ " in a symbolic list"
@@ -538,8 +538,8 @@ compileCoeffect (TyGrade k' 0) k vars = do
 
     (isSet -> Just (elemTy, polarity)) ->
       case polarity of
-        Normal   -> setEmpty polarity
-        Opposite -> setUniverse polarity elemTy
+        Normal   -> setUniverse polarity elemTy
+        Opposite -> setEmpty polarity
 
     (TyVar _) -> return (SUnknown (SynLeaf (Just 0)), sTrue)
 
@@ -578,8 +578,8 @@ compileCoeffect (TyGrade k' 1) k vars = do
 
     (isSet -> Just (elemTy, polarity)) ->
       case polarity of
-        Normal   -> setUniverse polarity elemTy
-        Opposite -> setEmpty polarity
+        Normal   -> setEmpty polarity
+        Opposite -> setUniverse polarity elemTy
 
     (TyVar _) -> return (SUnknown (SynLeaf (Just 1)), sTrue)
 
@@ -632,10 +632,10 @@ approximatedByOrEqualConstraint (SFloat n) (SFloat m)  = return $ n .<= m
 approximatedByOrEqualConstraint SPoint SPoint          = return $ sTrue
 approximatedByOrEqualConstraint (SOOZ s) (SOOZ r) = pure $ s .== r
 approximatedByOrEqualConstraint (SSet Normal s) (SSet Normal t) =
-  pure $ s `S.isSubsetOf` t
+  pure $ t `S.isSubsetOf` s
 
 approximatedByOrEqualConstraint (SSet Opposite s) (SSet Opposite t) =
-  pure $ t `S.isSubsetOf` s
+  pure $ s `S.isSubsetOf` t
 
 
 approximatedByOrEqualConstraint (SLevel l) (SLevel k) =

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

@@ -298,8 +298,8 @@ symGradeEq s t = solverError $ cannotDo ".==" s t
 -- | Meet operation on symbolic grades
 symGradeMeet :: SGrade -> SGrade -> Symbolic SGrade
 symGradeMeet (SNat n1) (SNat n2)     = return $ SNat $ n1 `smin` n2
-symGradeMeet (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
-symGradeMeet (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
+symGradeMeet (SSet Normal s) (SSet Normal t)     = return $ SSet Normal $ S.intersection s t
+symGradeMeet (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradeMeet (SLevel s) (SLevel t) =
   -- Using the join (!) from the Agda code (by cases)
   return $ SLevel $ ite (s .== literal unusedRepresentation) t -- join Unused x = x
@@ -334,8 +334,8 @@ symGradeMeet s t = solverError $ cannotDo "meet" s t
 -- | Join operation on symbolic grades
 symGradeJoin :: SGrade -> SGrade -> Symbolic SGrade
 symGradeJoin (SNat n1) (SNat n2) = return $ SNat (n1 `smax` n2)
-symGradeJoin (SSet Normal s) (SSet Normal t)   = return $ SSet Normal $ S.intersection s t
-symGradeJoin (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
+symGradeJoin (SSet Normal s) (SSet Normal t)     = return $ SSet Normal $ S.union s t
+symGradeJoin (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeJoin (SLevel s) (SLevel t) =
   -- Using the meet (!) from the Agda code (by cases)
   return $ SLevel $ ite (s .== literal unusedRepresentation) t -- meet Unused x = x
@@ -383,8 +383,8 @@ symGradeJoin s t = solverError $ cannotDo "join" s t
 -- | Plus operation on symbolic grades
 symGradePlus :: SGrade -> SGrade -> Symbolic SGrade
 symGradePlus (SNat n1) (SNat n2) = return $ SNat (n1 + n2)
-symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
-symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
+symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersection s t
+symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradePlus (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradePlus (SFloat n1) (SFloat n2) = return $ SFloat $ n1 + n2
 symGradePlus (SExtNat x) (SExtNat y) = return $ SExtNat (x + y)
@@ -432,8 +432,8 @@ symGradeTimes :: SGrade -> SGrade -> Symbolic SGrade
 symGradeTimes (SNat n1) (SNat n2) = return $ SNat (n1 * n2)
 symGradeTimes (SNat n1) (SExtNat (SNatX n2)) = return $ SExtNat $ SNatX (n1 * n2)
 symGradeTimes (SExtNat (SNatX n1)) (SNat n2) = return $ SExtNat $ SNatX (n1 * n2)
-symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersection s t
-symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
+symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
+symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeTimes (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradeTimes (SFloat n1) (SFloat n2) = return $ SFloat $ n1 * n2
 symGradeTimes (SExtNat x) (SExtNat y) = return $ SExtNat (x * y)

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

@@ -955,7 +955,7 @@ cProduct x y = TyApp (TyApp (TyCon (mkId ",,")) x) y
 -- | Find out whether a coeffect if flattenable, and if so get the operation
 -- | used to represent flattening on the grades
 flattenable :: (?globals :: Globals)
-            => Type -> Type -> Checker (Maybe ((Coeffect -> Coeffect -> Coeffect), Substitution, Type))
+            => Type -> Type -> Checker (Maybe (Coeffect -> Coeffect -> Coeffect, Substitution, Type))
 flattenable t1 t2
  | t1 == t2 = case t1 of
     t1 | t1 == extendedNat -> return $ Just (TyInfix TyOpTimes, [], t1)
@@ -969,7 +969,7 @@ flattenable t1 t2
     -- Sets can use multiply to fold two levels
     (isSet -> Just (elemType, polarity)) -> return $ Just (TyInfix TyOpTimes, [], t1)
 
-    _ -> return $ Nothing
+    _ -> return Nothing
  | otherwise =
       case (t1, t2) of
         (isInterval -> Just t, TyCon (internalName -> "LNL")) | t == extendedNat ->
@@ -1301,4 +1301,3 @@ instance Unifiable t => Unifiable (Maybe t) where
     unify' Nothing _ = return []
     unify' _ Nothing = return []
     unify' (Just x) (Just y) = unify' x y
-

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

@@ -371,7 +371,7 @@ ctxtFromTypedPattern' _ s _ t p _ = do
   debugM "dataConstructors in checker state" $ show $ dataConstructors st
   case t of
     (Star _ t') -> throw $ UniquenessError { errLoc = s, uniquenessMismatch = UniquePromotion t'}
-    otherwise -> throw $ PatternTypingError { errLoc = s, errPat = p, tyExpected = t }
+    _ -> throw PatternTypingError { errLoc = s, errPat = p, tyExpected = t }
 
 flattenCoeffects :: (?globals :: Globals) => Span -> Maybe (Coeffect, Type) -> Maybe (Coeffect, Type) -> Checker (Maybe (Coeffect, Type), Substitution)
 flattenCoeffects s Nothing Nothing | usingExtension GradedBase = do