cleanup old code

Author: dorchard

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

@@ -570,45 +570,6 @@ renameBeta oldName newName t =
       renamer :: Id -> Id
       renamer id = if id == oldName then newName else id
 
-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, [])
-
--- Check if `Rename id a ~ a'` which may involve some normalisation in the
 -- case where `a'` is a variable
 eqRenameFunction :: (?globals :: Globals)
   => Span
@@ -626,23 +587,6 @@ eqRenameFunction sp rel oldName newName t t' ind = do
   (eq, u) <- equalTypesRelatedCoeffects sp rel t'' t' ind Types
   return (eq, u)
 
--- eqRenameFunction sp rel name t (TyApp (TyApp (TyCon (internalName d -> "Rename")) name') t') ind = 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
---   (eq, u) <- equalTypesRelatedCoeffects sp rel t'' t' ind Types
---  return (eq, u)
-
 -- | Is this protocol dual to the other?
 isDualSession :: (?globals :: Globals)
     => Span

frontend/tests/cases/negative/graded/polySemiring.gr.output

@@ -1,6 +1,6 @@
-Type checking failed:
+Type checking failed: 
 Counter example: frontend/tests/cases/negative/graded/polySemiring.gr:2:1:
   When checking `foo`, (1 : s) + (1 : s) is not approximatable by r for type s
 
 Counter-example:
-  r = 3 :: s
+  r = 3 :: s

frontend/tests/cases/negative/graded/semiringsDontHaveCommutativeMult.gr.output

@@ -3,4 +3,4 @@ Counter example: frontend/tests/cases/negative/graded/semiringsDontHaveCommutati
   When checking `poly`, c * ((1 : k) + (1 : k)) is not approximatable by (((1 : k)) + ((1 : k))) * c for type k
 
 Counter-example:
-  c = 0 :: k
+  c = 3 :: k

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/negative/unique/uniqueProduct.gr.output

@@ -1,6 +1,3 @@
 Type checking failed: 
-Ownership error: frontend/tests/cases/negative/unique/uniqueProduct.gr:2:58:
-Cannot guarantee usage of reference to value of type `FloatArray id` at permission `Star`.
-
 Linearity error: frontend/tests/cases/negative/unique/uniqueProduct.gr:5:22:
 Linear variable `arrs` is used more than once.