From 662ab316c29aba7c433bdcbf78579e9bee176a1f Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 30 Jan 2026 13:15:05 +0100
Subject: [PATCH 1/6] Equality constraints

---
 src/Agda2Hs/Compile/Data.hs           |  2 +-
 src/Agda2Hs/Compile/Function.hs       |  4 ++-
 src/Agda2Hs/Compile/Record.hs         |  2 +-
 src/Agda2Hs/Compile/Term.hs           |  7 +++--
 src/Agda2Hs/Compile/Type.hs           | 40 ++++++++++++++++++++++-----
 src/Agda2Hs/Compile/TypeDefinition.hs |  2 +-
 src/Agda2Hs/Compile/Types.hs          |  8 ++++++
 src/Agda2Hs/Compile/Utils.hs          | 10 +++++++
 test/EqualityConstraint.agda          | 13 +++++++++
 test/EqualityConstraint.hs            |  9 ++++++
 test/EqualityExample.agda             | 21 ++++++++++++++
 test/EqualityExample.hs               |  9 ++++++
 test/ErasedTypeArguments.hs           | 11 ++++++++
 13 files changed, 125 insertions(+), 13 deletions(-)
 create mode 100644 test/EqualityConstraint.agda
 create mode 100644 test/EqualityConstraint.hs
 create mode 100644 test/EqualityExample.agda
 create mode 100644 test/EqualityExample.hs
 create mode 100644 test/ErasedTypeArguments.hs

diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs
index 5f710c49..425fab73 100644
--- a/src/Agda2Hs/Compile/Data.hs
+++ b/src/Agda2Hs/Compile/Data.hs
@@ -18,7 +18,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.AgdaUtils
 
 import Agda2Hs.Compile.Name
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index c64549d8..bad69366 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -38,7 +38,7 @@ import Agda.Utils.Size ( Sized(size) )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom )
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -257,6 +257,7 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
   (Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
     DODropped  -> False
     DOInstance -> True
+    DOEquality -> True
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
@@ -301,6 +302,7 @@ compilePats ty ((namedArg -> pat):ps) = do
   let rest = compilePats (absApp b (patternToTerm pat)) ps
   compileDom a >>= \case
     DOInstance -> rest
+    DOEquality -> rest
     DODropped  -> rest
     DOType     -> rest
     DOTerm     -> do
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index fd9193b3..3aa43102 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -24,7 +24,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.ClassInstance
 import Agda2Hs.Compile.Function ( compileFun )
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 0171b5bd..5176c9e7 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -41,7 +41,7 @@ import Agda.Utils.Size
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName, importInstance )
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize, compileDomType )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileTelSize, compileDomType )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
@@ -508,6 +508,7 @@ dependentDom dom = do
     DOTerm     -> False
     DOInstance -> False
     DODropped  -> False
+    DOEquality -> False
 
 compileLam :: Type -> ArgInfo -> Abs Term -> C (Hs.Exp ())
 compileLam ty argi abs = do
@@ -612,6 +613,7 @@ compileArgs' ty (x:xs) = do
   compileDom a >>= \case
     DODropped  -> rest
     DOInstance -> checkInstance x *> rest
+    DOEquality -> checkInstance x *> rest
     DOType     -> checkValidType x *> rest
     DOTerm     -> second . (:) <$> compileTerm (unDom a) x <*> rest
 
@@ -653,7 +655,8 @@ checkInstance u = do
     Con c _ _
       | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
         prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
-        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
+        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" ||
+        prettyShow (conName c) == "Agda.Builtin.Equality.refl" -> return ()
     _ -> illegalInstance
 
   where
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 74d2dcde..271c634c 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -14,7 +14,7 @@ import qualified Data.Set as Set ( singleton )
 import Agda.Compiler.Backend hiding ( Args )
 
 import Agda.Syntax.Common
-import Agda.Syntax.Internal
+import Agda.Syntax.Internal hiding (isEqualityType)
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
@@ -101,6 +101,7 @@ compileType t = do
         DomType _ hsA -> Hs.TyFun () hsA <$> compileB
         DomConstraint hsA -> constrainType hsA <$> compileB
         DomDropped -> compileB
+        DomEquality hsA -> constrainType hsA <$> compileB
         DomForall Nothing -> compileB
         DomForall (Just hsA) -> qualifyType hsA <$> compileB
 
@@ -122,7 +123,8 @@ compileType t = do
 
     Var x es | Just args <- allApplyElims es -> do
       CtxVar _ ti <- lookupBV x
-      unless (usableModality ti) $ agda2hsErrorM $
+      isType <- endsInSort (unDom ti)
+      unless (usableModality ti || isType) $ agda2hsErrorM $
             text "Cannot use erased variable" <+> prettyTCM (var x)
         <+> text "in Haskell type"
       vs <- compileTypeArgs (unDom ti) args
@@ -173,6 +175,7 @@ compileTel (ExtendTel a tel) = compileDom a >>= \case
   DOInstance -> __IMPOSSIBLE__
   DOType     -> __IMPOSSIBLE__
   DOTerm     -> (:) <$> compileType (unEl $ unDom a) <*> underAbstraction a tel compileTel
+  DOEquality -> __IMPOSSIBLE__
 
 -- Version of @compileTel@ that just computes the size,
 -- and avoids compiling the types themselves.
@@ -183,6 +186,7 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
   DOInstance -> __IMPOSSIBLE__
   DOType -> __IMPOSSIBLE__
   DOTerm -> (1+) <$> underAbstraction a tel compileTelSize
+  DOEquality -> __IMPOSSIBLE__
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
@@ -206,18 +210,20 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   []     -> __IMPOSSIBLE__
 
 
-data DomOutput = DOInstance | DODropped | DOType | DOTerm
+
 
 compileDom :: Dom Type -> C DomOutput
 compileDom a = do
   isErasable <- pure (not $ usableModality a) `or2M` canErase (unDom a)
   isClassConstraint <- pure (isInstance a) `and2M` isClassType (unDom a)
+  isEqualityConstraint <- pure (isInstance a) `and2M` isEqualityType (unDom a)
   isType <- endsInSort (unDom a)
   return $ if
-    | isErasable        -> DODropped
-    | isClassConstraint -> DOInstance
-    | isType            -> DOType
-    | otherwise         -> DOTerm
+    | isEqualityConstraint -> DOEquality
+    | isClassConstraint  -> DOInstance
+    | isErasable         -> DODropped
+    | isType             -> DOType
+    | otherwise          -> DOTerm
 
 -- | Compile a function type domain.
 -- A domain can either be:
@@ -231,6 +237,7 @@ compileDomType x a =
   compileDom a >>= \case
     DODropped  -> pure DomDropped
     DOInstance -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
+    DOEquality -> compileEqualityConstraint (unEl $ unDom a)
     DOType     -> do
       -- We compile (non-erased) type parameters to an explicit forall if they
       -- come from a module parameter or if we are in a nested position inside the type.
@@ -250,6 +257,24 @@ compileDomType x a =
         | otherwise -> return $ DomForall Nothing
     DOTerm     -> fmap (uncurry DomType) . withNestedType . compileTypeWithStrictness . unEl $ unDom a
 
+compileEqualityConstraint :: Term -> C CompiledDom
+compileEqualityConstraint t = do
+  t' <- reduce t
+  case t' of
+    Def f es -> do
+      eq <- liftTCM $ getBuiltinName' builtinEquality
+      if Just f == eq then do
+        tellExtension Hs.TypeOperators
+        -- The arguments to equality are _a_ (level), _A_ (the type of elements), x, and y
+        -- We want to compile x and y
+        let Just (_:_:x:y:_) = allApplyElims es
+        hsX <- compileType (unArg x)
+        hsY <- compileType (unArg y)
+        return $ DomEquality $ Hs.TypeA () $ Hs.TyInfix () hsX (Hs.UnpromotedName () (Hs.UnQual () (Hs.Symbol () "~"))) hsY
+      else
+        agda2hsErrorM $ text "Not an equality type:" <?> prettyTCM t
+    _ -> agda2hsErrorM $ text "Not an equality type:" <?> prettyTCM t
+
 compileTeleBinds :: Bool -> Telescope -> C [Hs.TyVarBind ()]
 compileTeleBinds kinded = go
   where
@@ -264,6 +289,7 @@ compileTeleBinds kinded = go
         (ha:) <$> underAbstraction a tel go
       DOInstance -> agda2hsError "Constraint in type parameter not supported"
       DOTerm -> agda2hsError "Term variable in type parameter not supported"
+      DOEquality -> agda2hsError "Equality constraint in type parameter not supported"
 
 compileKeptTeleBind :: Bool -> Hs.Name () -> Type -> C (Hs.TyVarBind ())
 compileKeptTeleBind kinded x t = do
diff --git a/src/Agda2Hs/Compile/TypeDefinition.hs b/src/Agda2Hs/Compile/TypeDefinition.hs
index 31533a03..7d087735 100644
--- a/src/Agda2Hs/Compile/TypeDefinition.hs
+++ b/src/Agda2Hs/Compile/TypeDefinition.hs
@@ -15,7 +15,7 @@ import Agda.TypeChecking.Telescope ( mustBePi )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Monad
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTypeArgs )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileTypeArgs )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 84be1b82..373fac56 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -199,6 +199,11 @@ instance Semigroup a => Semigroup (C a) where (<>) = liftA2 (<>)
 
 
 
+
+-- | Determines how a 'Dom Type' is treated during compilation.
+data DomOutput = DODropped | DOInstance | DOType | DOTerm | DOEquality
+
+-- | Determines how an argument is compiled.
 -- | Agda @Dom Type@ can get compiled in three ways.
 data CompiledDom
   = DomType Strictness (Hs.Type ())
@@ -209,6 +214,9 @@ data CompiledDom
     -- ^ To a forall, with an optional type variable declaration. If Nothing, this is an implicit forall; otherwise, explicit.
   | DomDropped
     -- ^ To nothing (e.g. erased proofs)
+  | DomEquality (Hs.Asst ())
+    -- ^ To an equality constraint (e.g. `(a ~ b)`)
+
 
 -- | Whether a datatype/record should be compiled as a @newtype@ haskell definition.
 type AsNewType = Bool
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index b228d0be..d8f91acd 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -233,6 +233,16 @@ isClassType a = do
     Def cl _ -> isClassName cl
     _        -> return False
 
+-- | Check if the given type corresponds to the Agda built-in equality.
+isEqualityType :: Type -> C Bool
+isEqualityType a = do
+  TelV _ t <- telView a
+  case unEl t of
+    Def f _ -> do
+      eq <- liftTCM $ getBuiltinName' builtinEquality
+      return $ Just f == eq
+    _ -> return False
+
 -- Drops the last (record) module for typeclass methods
 dropClassModule :: ModuleName -> C ModuleName
 dropClassModule m@(MName ns) = isClassModule m >>= \case
diff --git a/test/EqualityConstraint.agda b/test/EqualityConstraint.agda
new file mode 100644
index 00000000..a99f9bb9
--- /dev/null
+++ b/test/EqualityConstraint.agda
@@ -0,0 +1,13 @@
+module EqualityConstraint where
+
+open import Haskell.Prelude hiding (c)
+
+postulate
+  c : Type
+
+{-# COMPILE AGDA2HS c #-}
+
+postulate
+  myFunc : {@0 a b : Type} → ⦃ @0 p : a ≡ b ⦄ → c
+
+{-# COMPILE AGDA2HS myFunc #-}
diff --git a/test/EqualityConstraint.hs b/test/EqualityConstraint.hs
new file mode 100644
index 00000000..1ecb6125
--- /dev/null
+++ b/test/EqualityConstraint.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeOperators #-}
+module EqualityConstraint where
+
+c :: *
+c = error "postulate: *"
+
+myFunc :: a ~ b => c
+myFunc = error "postulate:   a ~ b => c"
+
diff --git a/test/EqualityExample.agda b/test/EqualityExample.agda
new file mode 100644
index 00000000..4a25f463
--- /dev/null
+++ b/test/EqualityExample.agda
@@ -0,0 +1,21 @@
+module EqualityExample where
+
+open import Haskell.Prelude
+open import Agda.Primitive using (Level)
+
+variable @0 ℓ : Level
+coerce' : {@0 a b : Type} → ⦃ @0 _ : a ≡ b ⦄ → a → b
+coerce' ⦃ refl ⦄ x = x
+{-# COMPILE AGDA2HS coerce' #-}
+
+instance
+  symType : {@0 a b : Type ℓ} → ⦃ @0 p : a ≡ b ⦄ → b ≡ a
+  symType ⦃ refl ⦄ = refl
+
+-- A function that requires two types to be equal to return a list of them.
+-- In Haskell, this corresponds to:
+-- sameList :: (a ~ b) => a -> b -> [a]
+-- sameList x y = [x, y]
+sameList : {@0 x y : Type} → ⦃ @0 p : x ≡ y ⦄ → x → y → List x
+sameList {x} {y} {{p}} vx vy = vx ∷ coerce' ⦃ symType ⦃ p ⦄ ⦄ vy ∷ []
+{-# COMPILE AGDA2HS sameList #-}
diff --git a/test/EqualityExample.hs b/test/EqualityExample.hs
new file mode 100644
index 00000000..87199028
--- /dev/null
+++ b/test/EqualityExample.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeOperators #-}
+module EqualityExample where
+
+coerce' :: a ~ b => a -> b
+coerce' x = x
+
+sameList :: x ~ y => x -> y -> [x]
+sameList vx vy = [vx, coerce' vy]
+
diff --git a/test/ErasedTypeArguments.hs b/test/ErasedTypeArguments.hs
new file mode 100644
index 00000000..da07ad41
--- /dev/null
+++ b/test/ErasedTypeArguments.hs
@@ -0,0 +1,11 @@
+module ErasedTypeArguments where
+
+import Numeric.Natural (Natural)
+
+data Σ' a b = (:^:){proj₁ :: a, proj₂ :: b}
+
+test :: Natural -> Σ' Natural ()
+test n = n :^: ()
+
+newtype Id f = MkId f
+

From 728c4c7ab8ff5affe8ad15083bd6b302776de265 Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 6 Mar 2026 14:11:31 +0100
Subject: [PATCH 2/6] Un-shadow isEqualityType and simplify
 compileEqualityConstraint

---
 src/Agda2Hs/Compile/Type.hs  | 30 ++++++++++--------------------
 src/Agda2Hs/Compile/Types.hs |  3 ---
 src/Agda2Hs/Compile/Utils.hs |  8 ++++----
 3 files changed, 14 insertions(+), 27 deletions(-)

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 271c634c..08a263e8 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -14,7 +14,7 @@ import qualified Data.Set as Set ( singleton )
 import Agda.Compiler.Backend hiding ( Args )
 
 import Agda.Syntax.Common
-import Agda.Syntax.Internal hiding (isEqualityType)
+import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
@@ -209,14 +209,11 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs
   []     -> __IMPOSSIBLE__
 
-
-
-
 compileDom :: Dom Type -> C DomOutput
 compileDom a = do
   isErasable <- pure (not $ usableModality a) `or2M` canErase (unDom a)
   isClassConstraint <- pure (isInstance a) `and2M` isClassType (unDom a)
-  isEqualityConstraint <- pure (isInstance a) `and2M` isEqualityType (unDom a)
+  isEqualityConstraint <- pure (isInstance a) `and2M` isBuiltinEqualityType (unDom a)
   isType <- endsInSort (unDom a)
   return $ if
     | isEqualityConstraint -> DOEquality
@@ -259,21 +256,14 @@ compileDomType x a =
 
 compileEqualityConstraint :: Term -> C CompiledDom
 compileEqualityConstraint t = do
-  t' <- reduce t
-  case t' of
-    Def f es -> do
-      eq <- liftTCM $ getBuiltinName' builtinEquality
-      if Just f == eq then do
-        tellExtension Hs.TypeOperators
-        -- The arguments to equality are _a_ (level), _A_ (the type of elements), x, and y
-        -- We want to compile x and y
-        let Just (_:_:x:y:_) = allApplyElims es
-        hsX <- compileType (unArg x)
-        hsY <- compileType (unArg y)
-        return $ DomEquality $ Hs.TypeA () $ Hs.TyInfix () hsX (Hs.UnpromotedName () (Hs.UnQual () (Hs.Symbol () "~"))) hsY
-      else
-        agda2hsErrorM $ text "Not an equality type:" <?> prettyTCM t
-    _ -> agda2hsErrorM $ text "Not an equality type:" <?> prettyTCM t
+  Def _ es <- reduce t
+  tellExtension Hs.TypeOperators
+  -- The arguments to equality are _a_ (level), _A_ (the type of elements), x, and y
+  -- We want to compile x and y
+  let Just (_:_:x:y:_) = allApplyElims es
+  hsX <- compileType (unArg x)
+  hsY <- compileType (unArg y)
+  return $ DomEquality $ Hs.TypeA () $ Hs.TyInfix () hsX (Hs.UnpromotedName () (Hs.UnQual () (Hs.Symbol () "~"))) hsY
 
 compileTeleBinds :: Bool -> Telescope -> C [Hs.TyVarBind ()]
 compileTeleBinds kinded = go
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 373fac56..ad3508a0 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -197,9 +197,6 @@ instance Null a => Null (C a) where
   null = __IMPOSSIBLE__
 instance Semigroup a => Semigroup (C a) where (<>) = liftA2 (<>)
 
-
-
-
 -- | Determines how a 'Dom Type' is treated during compilation.
 data DomOutput = DODropped | DOInstance | DOType | DOTerm | DOEquality
 
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index d8f91acd..7b4756c5 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -234,13 +234,13 @@ isClassType a = do
     _        -> return False
 
 -- | Check if the given type corresponds to the Agda built-in equality.
-isEqualityType :: Type -> C Bool
-isEqualityType a = do
+isBuiltinEqualityType :: Type -> C Bool
+isBuiltinEqualityType a = do
   TelV _ t <- telView a
   case unEl t of
     Def f _ -> do
-      eq <- liftTCM $ getBuiltinName' builtinEquality
-      return $ Just f == eq
+      name <- getBuiltinName' builtinEquality
+      return $ Just f == name
     _ -> return False
 
 -- Drops the last (record) module for typeclass methods

From 6fbc63e6bbfbea3ff6db95f20df18394016208c8 Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 6 Mar 2026 18:04:10 +0100
Subject: [PATCH 3/6] Require equality constraints to be not marked erased

---
 src/Agda2Hs/Compile/Type.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 08a263e8..1049030c 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -123,8 +123,7 @@ compileType t = do
 
     Var x es | Just args <- allApplyElims es -> do
       CtxVar _ ti <- lookupBV x
-      isType <- endsInSort (unDom ti)
-      unless (usableModality ti || isType) $ agda2hsErrorM $
+      unless (usableModality ti) $ agda2hsErrorM $
             text "Cannot use erased variable" <+> prettyTCM (var x)
         <+> text "in Haskell type"
       vs <- compileTypeArgs (unDom ti) args
@@ -190,6 +189,7 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
+  reportSDoc "agda2hs" 1 $ text "compileUnboxType r=" <+> prettyTCM r <+> text " pars=" <+> prettyTCM pars
   def <- getConstInfo r
   let tel = recTel (theDef def) `apply` pars
   compileTel tel >>= \case
@@ -213,7 +213,7 @@ compileDom :: Dom Type -> C DomOutput
 compileDom a = do
   isErasable <- pure (not $ usableModality a) `or2M` canErase (unDom a)
   isClassConstraint <- pure (isInstance a) `and2M` isClassType (unDom a)
-  isEqualityConstraint <- pure (isInstance a) `and2M` isBuiltinEqualityType (unDom a)
+  isEqualityConstraint <- pure (usableModality a) `and2M` pure (isInstance a) `and2M` isBuiltinEqualityType (unDom a)
   isType <- endsInSort (unDom a)
   return $ if
     | isEqualityConstraint -> DOEquality

From 1ef0174871e58f324dbe4a65c3b701bec8dff85a Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 6 Mar 2026 18:29:42 +0100
Subject: [PATCH 4/6] Move test for equality constraint to Success directory

---
 test/EqualityConstraint.agda             | 13 -------------
 test/EqualityExample.agda                | 21 ---------------------
 test/EqualityExample.hs                  |  9 ---------
 test/Succeed/EqualityConstraint.agda     |  8 ++++++++
 test/{ => Succeed}/EqualityConstraint.hs |  3 ---
 5 files changed, 8 insertions(+), 46 deletions(-)
 delete mode 100644 test/EqualityConstraint.agda
 delete mode 100644 test/EqualityExample.agda
 delete mode 100644 test/EqualityExample.hs
 create mode 100644 test/Succeed/EqualityConstraint.agda
 rename test/{ => Succeed}/EqualityConstraint.hs (79%)

diff --git a/test/EqualityConstraint.agda b/test/EqualityConstraint.agda
deleted file mode 100644
index a99f9bb9..00000000
--- a/test/EqualityConstraint.agda
+++ /dev/null
@@ -1,13 +0,0 @@
-module EqualityConstraint where
-
-open import Haskell.Prelude hiding (c)
-
-postulate
-  c : Type
-
-{-# COMPILE AGDA2HS c #-}
-
-postulate
-  myFunc : {@0 a b : Type} → ⦃ @0 p : a ≡ b ⦄ → c
-
-{-# COMPILE AGDA2HS myFunc #-}
diff --git a/test/EqualityExample.agda b/test/EqualityExample.agda
deleted file mode 100644
index 4a25f463..00000000
--- a/test/EqualityExample.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-module EqualityExample where
-
-open import Haskell.Prelude
-open import Agda.Primitive using (Level)
-
-variable @0 ℓ : Level
-coerce' : {@0 a b : Type} → ⦃ @0 _ : a ≡ b ⦄ → a → b
-coerce' ⦃ refl ⦄ x = x
-{-# COMPILE AGDA2HS coerce' #-}
-
-instance
-  symType : {@0 a b : Type ℓ} → ⦃ @0 p : a ≡ b ⦄ → b ≡ a
-  symType ⦃ refl ⦄ = refl
-
--- A function that requires two types to be equal to return a list of them.
--- In Haskell, this corresponds to:
--- sameList :: (a ~ b) => a -> b -> [a]
--- sameList x y = [x, y]
-sameList : {@0 x y : Type} → ⦃ @0 p : x ≡ y ⦄ → x → y → List x
-sameList {x} {y} {{p}} vx vy = vx ∷ coerce' ⦃ symType ⦃ p ⦄ ⦄ vy ∷ []
-{-# COMPILE AGDA2HS sameList #-}
diff --git a/test/EqualityExample.hs b/test/EqualityExample.hs
deleted file mode 100644
index 87199028..00000000
--- a/test/EqualityExample.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-module EqualityExample where
-
-coerce' :: a ~ b => a -> b
-coerce' x = x
-
-sameList :: x ~ y => x -> y -> [x]
-sameList vx vy = [vx, coerce' vy]
-
diff --git a/test/Succeed/EqualityConstraint.agda b/test/Succeed/EqualityConstraint.agda
new file mode 100644
index 00000000..9863611d
--- /dev/null
+++ b/test/Succeed/EqualityConstraint.agda
@@ -0,0 +1,8 @@
+module EqualityConstraint where
+
+open import Haskell.Prelude
+
+postulate
+  myFunc : ⦃ p : a ≡ b ⦄ → c
+
+{-# COMPILE AGDA2HS myFunc #-}
diff --git a/test/EqualityConstraint.hs b/test/Succeed/EqualityConstraint.hs
similarity index 79%
rename from test/EqualityConstraint.hs
rename to test/Succeed/EqualityConstraint.hs
index 1ecb6125..c7434c92 100644
--- a/test/EqualityConstraint.hs
+++ b/test/Succeed/EqualityConstraint.hs
@@ -1,9 +1,6 @@
 {-# LANGUAGE TypeOperators #-}
 module EqualityConstraint where
 
-c :: *
-c = error "postulate: *"
-
 myFunc :: a ~ b => c
 myFunc = error "postulate:   a ~ b => c"
 

From 7c03af7df98dcc98c19521a724d181f8c113d748 Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 6 Mar 2026 18:40:55 +0100
Subject: [PATCH 5/6] Remove debugging log and unecessary tellExtension

---
 src/Agda2Hs/Compile/Type.hs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 1049030c..039bb4d4 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -189,7 +189,6 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
-  reportSDoc "agda2hs" 1 $ text "compileUnboxType r=" <+> prettyTCM r <+> text " pars=" <+> prettyTCM pars
   def <- getConstInfo r
   let tel = recTel (theDef def) `apply` pars
   compileTel tel >>= \case
@@ -257,8 +256,7 @@ compileDomType x a =
 compileEqualityConstraint :: Term -> C CompiledDom
 compileEqualityConstraint t = do
   Def _ es <- reduce t
-  tellExtension Hs.TypeOperators
-  -- The arguments to equality are _a_ (level), _A_ (the type of elements), x, and y
+  -- The arguments to equality are _a_ (level), _A_ (the type of elements), x (: A), and y (: A)
   -- We want to compile x and y
   let Just (_:_:x:y:_) = allApplyElims es
   hsX <- compileType (unArg x)

From b4cc12ab00249b109ecdaae68903eeaa76f536d2 Mon Sep 17 00:00:00 2001
From: Ridan Vandenbergh <ridanvandenbergh@gmail.com>
Date: Fri, 6 Mar 2026 19:08:04 +0100
Subject: [PATCH 6/6] Remove leftover test .hs file

---
 test/ErasedTypeArguments.hs | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 test/ErasedTypeArguments.hs

diff --git a/test/ErasedTypeArguments.hs b/test/ErasedTypeArguments.hs
deleted file mode 100644
index da07ad41..00000000
--- a/test/ErasedTypeArguments.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-module ErasedTypeArguments where
-
-import Numeric.Natural (Natural)
-
-data Σ' a b = (:^:){proj₁ :: a, proj₂ :: b}
-
-test :: Natural -> Σ' Natural ()
-test n = n :^: ()
-
-newtype Id f = MkId f
-