Use expression equivalence instead of Haskell equality

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -95,7 +95,7 @@ checkAnomaByteArrayToAnomaContents f = do
   byteArray <- getBuiltinNameScoper l BuiltinByteArray
   nat_ <- getBuiltinNameScoper l BuiltinNat
   unless
-    (ftype == (byteArray --> nat_))
+    (ftype === (byteArray --> nat_))
     $ builtinsErrorText l "toAnomaContents must be of type ByteArray -> Nat"
 
 checkAnomaByteArrayFromAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
@@ -105,7 +105,7 @@ checkAnomaByteArrayFromAnomaContents f = do
   byteArray <- getBuiltinNameScoper l BuiltinByteArray
   nat_ <- getBuiltinNameScoper l BuiltinNat
   unless
-    (ftype == (nat_ --> nat_ --> byteArray))
+    (ftype === (nat_ --> nat_ --> byteArray))
     $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"
 
 checkAnomaSha256 :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
@@ -115,7 +115,7 @@ checkAnomaSha256 f = do
   byteArray <- getBuiltinNameScoper l BuiltinByteArray
   nat_ <- getBuiltinNameScoper l BuiltinNat
   unless
-    (ftype == (nat_ --> byteArray))
+    (ftype === (nat_ --> byteArray))
     $ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray"
 
 checkResource :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
@@ -257,23 +257,23 @@ checkAnomaIsCommitment f = do
   let l = getLoc f
   nat_ <- getBuiltinNameScoper l BuiltinNat
   bool_ <- getBuiltinNameScoper l BuiltinBool
-  unless (f ^. axiomType == (nat_ --> bool_)) $
+  unless (f ^. axiomType === (nat_ --> bool_)) $
     builtinsErrorText l "isCommitment must be of type Nat -> Bool"
 
 checkAnomaIsNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
 checkAnomaIsNullifier f = do
   let l = getLoc f
   nat_ <- getBuiltinNameScoper l BuiltinNat
   bool_ <- getBuiltinNameScoper l BuiltinBool
-  unless (f ^. axiomType == (nat_ --> bool_)) $
+  unless (f ^. axiomType === (nat_ --> bool_)) $
     builtinsErrorText l "isNullifier must be of type Nat -> Bool"
 
 checkAnomaSet :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
 checkAnomaSet t = do
   let ty = t ^. axiomType
       l = getLoc t
       u = ExpressionUniverse smallUniverseNoLoc
-  unless (ty == (u --> u)) $
+  unless (ty === (u --> u)) $
     builtinsErrorText l "AnomaSet should have type: Type -> Type"
 
 checkAnomaSetToList :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -711,6 +711,7 @@ matchExpressions = go
     -- Soft free vars are allowed to be matched
     isSoftFreeVar :: VarName -> Sem r Bool
     isSoftFreeVar = asks . HashSet.member
+
     go :: Expression -> Expression -> Sem r ()
     go a b = case (a, b) of
       (ExpressionIden ia, ExpressionIden ib) -> case (ia, ib) of
@@ -805,8 +806,10 @@ matchFunctionParameter pa pb = do
   where
     goParamType :: Expression -> Expression -> Sem r ()
     goParamType ua ub = matchExpressions ua ub
+
     goParamImplicit :: IsImplicit -> IsImplicit -> Sem r ()
     goParamImplicit ua ub = unless (ua == ub) (throw @Text "implicit mismatch")
+
     goParamName :: Maybe VarName -> Maybe VarName -> Sem r ()
     goParamName (Just va) (Just vb) = addName va vb
     goParamName _ _ = return ()