Improve Rename in clone, and fix uniqueness laws (#296)

* update test

* litmuss test

* wip on trying to improving the renamer in types

* fix clone law example

* unitR law no longer possible

* extra debug info

* kind based tests

* nub out repeated vars

* nit

* fix assoc typing

* cleanup old code

Author: dorchard

examples/uniqueness.gr

@@ -32,17 +32,13 @@ fst (a, b) = let !u = share b in a
 goodDesire : *Cake -> (Happy, Cake)
 goodDesire uniqueCake = let !cake = share uniqueCake in (eat cake, have cake)
 
--- Copying a non-linear value as unique and then borrowing it gives you the
--- original value
-unitR : forall {a : Type} . !a -> !a
-unitR t = clone t as x in share x
-
 -- Borrowing a unique value and copying it to apply a function is the same as
--- just applying the function
-unitL : forall {a b : Type} . *a -> (!a -> !b) -> !b
-unitL t f = clone (share t) as x in f (share x)
+-- -- just applying the function
+unitL : forall {a b : Type, id : Name} .
+          *(FloatArray id) -> (exists {id1 : Name} . *(FloatArray id1) -> b) -> b
+unitL t f = clone (share t) as x in f x
 
 -- Nesting copies works as you would expect (and obeys associativity)
-assoc : forall {a b c : Type} . !a -> (*a -> !b) -> (*b -> !c) -> !c
+assoc : forall {a b c : Type} . {Cloneable a, Cloneable b} => !a -> (*a -> !b) -> (*b -> !c) -> !c
 assoc t f g = clone t as x in 
                 clone f x as y in g y

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

@@ -674,6 +674,8 @@ checkExpr defs gam pol topLevel tau
   debugM "checkExpr[Clone]" (pretty s <> " : " <> pretty tau)
   (tau', gam, subst, elab) <- synthExpr defs gam pol expr
   -- Check the return types match
+  debugM "checkExpr[Clone]-types" $
+    "Expected: " <> pretty tau <> ", Synthesised: " <> pretty tau'
   (eqT, _, substTy) <- equalTypes s tau tau'
   unless eqT $ throw TypeError{ errLoc = s, tyExpected = tau, tyActual = tau' }
   substF <- combineSubstitutions s subst substTy
@@ -940,26 +942,47 @@ synthExpr _ _ _ (Val s _ rf (StringLiteral c)) = do
 
 -- Clone
 -- Pattern match on an applicable of `uniqueBind fun e`
+--------------------------------------
+--    G1, id |- e : [] r A
+--    G2, x : exists id' . *(A[id'/id])  |- body : B
+--    cloneable(A)
+--    1 <= r
+--- ------------------------------------------------
+----   (G1 + G2), id |- clone e as x in body : B
+---------------------------------------
 synthExpr defs gam pol
    expr@(App s a rf
      (App _ _ _
        (Val _ _ _ (Var _ (internalName -> "uniqueBind")))
        (Val _ _ _ (Abs _ (PVar _ _ _ var) _ body)))
      e) = do
-  debugM "synthExpr[uniqueBind]" (pretty s <> pretty expr)
+  debugM "synthExpr[Clone]" (pretty s <> pretty expr)
   -- Infer the type of e (the boxed argument)
   (ty, ghostVarCtxt, subst0, elabE) <- synthExpr defs gam pol e
-  -- Check that ty is actually a boxed type
+  -- Check that ty is actually a boxed type `[] r A`
   case ty of
     Box r tyA -> do
-      -- existential type for the cloned var ((exists {id : Name} . *(Rename id a))
-      idVar <- mkId <$> freshIdentifierBase "id"
+      -- extract every type var of kind `Name` from `tyA`
+      idVars <- typeVarsOfKind tyA (TyCon $ mkId "Name")
+      debugM "synthExpr[Clone]typeVars" (pretty idVars)
+      -- existential type for the cloned var ((exists {id' : Name} . *(Rename id' a))
+
+      -- make a fresh var for each of idVars
+      newIdVars <- mapM (\x -> freshIdentifierBase (internalName x) >>= (return . mkId)) idVars
+
+      -- apply the renamer for each of the idVars
+      let renamer (old, new) t = TyApp (TyApp (TyCon $ mkId "Rename") (TyVar old)) (TyVar new) `TyApp` t
+      let newAndOldVars = zip idVars newIdVars
+      let renamedTyA    = foldr renamer tyA newAndOldVars
+      -- Construct the cloned input type
       let clonedInputTy =
-            TyExists idVar (TyCon $ mkId "Name")
-              (Borrow (TyCon $ mkId "Star") (TyApp (TyApp (TyCon $ mkId "Rename") (TyVar idVar)) tyA))
+            foldr (\ idVar ty -> TyExists idVar (TyCon $ mkId "Name") ty)
+                (Borrow (TyCon $ mkId "Star") renamedTyA) newIdVars
+
+      -- cloned assumption
       let clonedAssumption = (var, Linear clonedInputTy)
 
-      debugM "synthExpr[uniqueBind]body" (pretty clonedAssumption)
+      debugM "synthExpr[Clone]body" (pretty clonedAssumption)
       -- synthesise the type of the body for the clone
       (tyB, ghostVarCtxt', subst1, elabBody) <- synthExpr defs (clonedAssumption : gam) pol body
 

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

@@ -17,7 +17,7 @@ import Control.Monad.State.Strict
 import Control.Monad.Trans.Maybe
 import Data.Functor.Identity (runIdentity)
 import Data.Maybe (fromMaybe)
-import Data.List (isPrefixOf, sortBy)
+import Data.List (isPrefixOf, sortBy, (\\), nub)
 
 import Language.Granule.Context
 
@@ -1377,3 +1377,42 @@ instance Unifiable t => Unifiable (Maybe t) where
     unify' Nothing _ = return []
     unify' _ Nothing = return []
     unify' (Just x) (Just y) = unify' x y
+
+-- Given a type, extract all the type variables which have
+-- the given kind
+typeVarsOfKind :: (?globals :: Globals) => Type -> Kind -> Checker [Id]
+typeVarsOfKind t k = do
+    vars <- typeFoldM algebra t 
+    return (nub vars)
+  where
+    algebra = TypeFold
+      { tfTy = \_ -> return []
+      , tfFunTy = \_ _ x y -> return (x ++ y)
+      , tfTyCon = \_ -> return []
+      , tfBox = \_ x -> return x
+      , tfDiamond = \_ x -> return x
+      , tfStar = \_ x -> return x
+      , tfBorrow = \_ x -> return x
+      , tfTyVar = \v -> do
+        -- Synth the kind of this type variable
+        synthKind nullSpan (TyVar v) >>= \case
+            -- check for equality with the argument
+          (k', subst , _) | k' == k -> do
+            when (not (null subst)) (debugM "[WARNING]" ("type variable " <> pretty v <> " has kind " <> pretty k <> " but its kind required a substitution which is being ignored during kind variable extraction"))
+            return [v]
+            -- kinds don't match
+          _                    -> return []
+      , tfTyApp = \ x y -> return (x ++ y)
+      , tfTyInt = \_ -> return []
+      , tfTyRational = \_ -> return []
+      , tfTyFraction = \_ -> return []
+      , tfTyGrade = \_ _ -> return []
+      , tfTyInfix = \_ x y -> return (x ++ y)
+      , tfSet = \ _ x -> return (concat x)
+      , tfTyCase = \ x branches ->
+          return (x ++ concatMap snd branches)
+      , tfTySig = \ x y -> (\_-> return x)
+      , tfTyExists = \ v k x -> return (x \\ [v])
+      , tfTyForall = \ v k x -> return (x \\ [v])
+      , tfTyName = \ _ -> return []
+      }

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

@@ -86,7 +86,7 @@ typeConstructors =
     , (mkId "ReceivePrefix", (funTy (tyCon "Protocol") (tyCon "Predicate"), [], [0]))
     , (mkId "Sends", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Predicate")), [], [0]))
     , (mkId "Graded", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Protocol")), [], [0]))
-    , (mkId "Rename", (funTy (tyCon "Name") (funTy (Type 0) (Type 0)), [], [0]))
+    , (mkId "Rename", (funTy (tyCon "Name") (funTy (tyCon "Name") (funTy (Type 0) (Type 0))), [], [0]))
     -- # Coeffect types
     , (mkId "Nat",      (kcoeffect, [], []))
     , (mkId "Q",        (kcoeffect, [], [])) -- Rationals

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

@@ -245,16 +245,16 @@ equalTypesRelatedCoeffectsInner s rel (Borrow p1 t1) (Borrow p2 t2) _ sp Types =
   u <- combineSubstitutions s unif unif'
   return (eq && eq', u)
 
+-- Handle equality involving renaming
+equalTypesRelatedCoeffectsInner s rel
+   t0@(TyApp (TyApp (TyApp (TyCon (internalName -> "Rename")) (TyVar oldName)) (TyVar newName)) t) t' ind sp mode = do
+    debugM "RenameL" (pretty t0 <> " = " <> pretty t')
+    eqRenameFunction s rel oldName newName t t' sp
 
-equalTypesRelatedCoeffectsInner s rel t0@(TyApp (TyApp (TyCon d) name) t) t' ind sp mode
-  | internalName d == "Rename" = do
-    debugM "RenameL" (pretty t <> " = " <> pretty t')
-    eqRenameFunction s rel name t t' sp
-
-equalTypesRelatedCoeffectsInner s rel t' t0@(TyApp (TyApp (TyCon d) name) t) ind sp mode
-  | internalName d == "Rename" = do
-    debugM "RenameR" (pretty t <> " = " <> pretty t')
-    eqRenameFunction s rel name t t' sp
+equalTypesRelatedCoeffectsInner s rel t' 
+  t0@(TyApp (TyApp (TyApp (TyCon (internalName -> "Rename")) (TyVar oldName)) (TyVar newName)) t) ind sp mode = do
+    debugM "RenameR" (pretty t' <> " = " <> pretty t0)
+    eqRenameFunction s rel oldName newName t t' sp
 
 -- ## GENERAL EQUALITY
 
@@ -557,102 +557,33 @@ eqGradedProtocolFunction sp rel grad (TyVar v) t ind = do
 eqGradedProtocolFunction sp _ grad t1 t2 _ = throw
   TypeError{ errLoc = sp, tyExpected = (TyApp (TyApp (TyCon $ mkId "Graded") grad) t1), tyActual = t2 }
 
--- Compute the behaviour of `Rename id a` on a type `A`
-renameBeta :: (?globals :: Globals)
-  => Type -- name
+-- Compute the behaviour of `Rename oldId newId a`
+-- where the arguments here are `oldId`, `newId` and `a`
+renameBeta ::
+     Id -- oldName
+  -> Id -- newName
   -> Type -- type
   -> Checker Type
-renameBeta name (TyApp (TyApp (TyCon c) t) s)
-  | internalName c == "Ref" = do
-    s' <- renameBeta name s
-    return $ (TyApp (TyApp (TyCon c) name) s')
-
-renameBeta name (TyApp (TyCon c) t)
-  | internalName c == "FloatArray" = do
-    return $ (TyApp (TyCon c) name)
-
-renameBeta name (TyApp (TyApp (TyCon c) t1) t2)
-  | internalName c == "," = do
-  t1' <- renameBeta name t1
-  t2' <- renameBeta name t2
-  return $ (TyApp (TyApp (TyCon c) t1') t2')
-
-renameBeta name (Star g t) = do
-  t' <- renameBeta name t
-  return $ (Star g t')
-
-renameBeta name (Borrow p t) = do
-  t' <- renameBeta name t
-  return $ (Borrow p t')
-
-renameBeta name t = return t
-
-renameBetaInvert :: (?globals :: Globals)
-  => Span
-  -- Explain how coeffects should be related by a solver constraint
-  -> (Span -> Coeffect -> Coeffect -> Type -> Constraint)
-  -> Type -- name
-  -> Type -- type
-  -- Indicates whether the first type or second type is a specification
-  -> SpecIndicator
-  -- Flag to say whether this type is actually an effect or not
-  -> Mode
-  -> Checker (Type, Substitution)
-
--- Ref case
--- i.e., Rename id a = Ref id' a'
--- therefore check `id ~ id'` and then recurse
-renameBetaInvert sp rel name (TyApp (TyApp (TyCon c) name') s) spec mode
-  | internalName c == "Ref" = do
-    -- Compute equality on names
-    (_, subst) <- equalTypesRelatedCoeffects sp rel name name' spec mode
-    (s, subst') <- renameBetaInvert sp rel name s spec mode
-    substFinal <- combineSubstitutions sp subst subst'
-    return (TyApp (TyApp (TyCon c) name') s, substFinal)
-
-renameBetaInvert sp rel name (TyApp (TyCon c) name') spec mode
-  | internalName c == "FloatArray" = do
-    -- Compute equality on names
-    (_, subst) <- equalTypesRelatedCoeffects sp rel name name' spec mode
-    return (TyApp (TyCon c) name', subst)
-
-renameBetaInvert sp rel name (TyApp (TyApp (TyCon c) t1) t2) spec mode
-  | internalName c == "," = do
-    (t1', subst1) <- renameBetaInvert sp rel name t1 spec mode
-    (t2', subst2) <- renameBetaInvert sp rel name t2 spec mode
-    substFinal <- combineSubstitutions sp subst1 subst2
-    return (TyApp (TyApp (TyCon c) t1') t2', substFinal)
-
-renameBetaInvert _ _ name t _ _ = return (t, [])
+renameBeta oldName newName t = 
+  typeFoldM (baseTypeFold { tfTyVar = return . TyVar . renamer }) t
+    where
+      renamer :: Id -> Id
+      renamer id = if id == oldName then newName else id
 
--- Check if `Rename id a ~ a'` which may involve some normalisation in the
 -- case where `a'` is a variable
 eqRenameFunction :: (?globals :: Globals)
   => Span
   -> (Span -> Coeffect -> Coeffect -> Type -> Constraint)
   -- These two arguments are the arguments to `Rename id a`
-  -> Type -- name
+  -> Id -- oldName
+  -> Id -- newName
   -> Type -- type
   -- This is the argument of the type which we are trying to see if it equal to `Rename id a`
   -> Type -- compared against
   -> SpecIndicator
   -> Checker (Bool, Substitution)
-
-eqRenameFunction sp rel name t (TyApp (TyApp (TyCon d) name') t') ind
-  | internalName d == "Rename" = do
-  (_, subst) <- equalTypesRelatedCoeffects sp rel name name' ind Types
-  (eq, subst') <- eqRenameFunction sp rel name t t' ind
-  substFinal <- combineSubstitutions sp subst subst'
-  return (eq, substFinal)
-
-eqRenameFunction sp rel name (TyVar v) t ind = do
-  (t', subst) <- renameBetaInvert sp rel name t ind Types
-  (eq, subst') <- equalTypesRelatedCoeffects sp rel t' (TyVar v) ind Types
-  substFinal <- combineSubstitutions sp subst subst'
-  return (eq, substFinal)
-
-eqRenameFunction sp rel name t t' ind = do
-  t'' <- renameBeta name t
+eqRenameFunction sp rel oldName newName t t' ind = do
+  t'' <- renameBeta oldName newName t
   (eq, u) <- equalTypesRelatedCoeffects sp rel t'' t' ind Types
   return (eq, u)
 
@@ -825,3 +756,4 @@ isPermission s ty = do
       putChecker
       return $ Right pTy
     Left err -> return $ Left pTy
+

frontend/tests/cases/negative/unique/cloneNonCloneable.gr

@@ -1,4 +1,4 @@
 example : Int [1]
 example =
   clone [42] as x
-    in (unpack <id' , a'> = x in (share a'))
+    in (unpack <id' , a'> = x in (share a'))

frontend/tests/cases/negative/unique/cloneNonCloneable.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
-Type constraint error: frontend/tests/cases/negative/unique/cloneNonCloneable.gr:1:1:
-Constraint `Cloneable Int` does not hold or is not provided by the type constraint assumptions here.
+Type error: frontend/tests/cases/negative/unique/cloneNonCloneable.gr:4:9:
+Expcted an existential type on the left-hand side of unpack, but got `*Int`

frontend/tests/cases/positive/unique/cloneLaw.gr

@@ -0,0 +1,3 @@
+unitL : forall {a b : Type, id : Name} .
+          *(FloatArray id) -> (exists {id1 : Name} . *(FloatArray id1) -> b) -> b
+unitL t f = clone (share t) as x in f x