From a610207304ab8081c13e6cf582cfc2f6363d1c8c Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 10 Sep 2024 17:14:25 +0200
Subject: [PATCH] [ re #354 ] Do not check canonicity of erased instances

---
 src/Agda2Hs/Compile/Utils.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index e43d1c8e..a8225a1b 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -261,10 +261,9 @@ checkInstance u = do
     checkInstanceElims = mapM_ checkInstanceElim
 
     checkInstanceElim :: Elim -> C ()
-    checkInstanceElim (Apply v) = case getHiding v of
-      Instance{} -> checkInstance $ unArg v
-      Hidden     -> return ()
-      NotHidden  -> return ()
+    checkInstanceElim (Apply v) =
+      when (isInstance v && usableQuantity v) $
+        checkInstance $ unArg v
     checkInstanceElim IApply{} = illegalInstance
     checkInstanceElim (Proj _ f) =
       unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance