From 001f8457d1d6d895497781bb1b0bfb8d738d834a Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Fri, 15 Mar 2024 17:05:15 +0100
Subject: [PATCH] Do not drop instance clauses but instead check canonicity

This was a regression introduced by https://github.com/agda/agda2hs/pull/304 that went unnoticed due to a lack of a (failing) test case
---
 src/Agda2Hs/Compile/ClassInstance.hs   |  4 ++--
 src/Agda2Hs/Compile/Function.hs        |  2 +-
 test/AllFailTests.agda                 |  1 +
 test/Fail/NonCanonicalSuperclass.agda  | 32 ++++++++++++++++++++++++++
 test/golden/NonCanonicalSuperclass.err |  2 ++
 5 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 test/Fail/NonCanonicalSuperclass.agda
 create mode 100644 test/golden/NonCanonicalSuperclass.err

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 2841f224..21e5b436 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -235,13 +235,13 @@ compileInstanceClause' curModule ty (p:ps) c
         reportSDoc "agda2hs.compile.instance" 20 $
           text $ "raw projection:" ++ prettyShow (Def n [])
         d <- chaseDef n
-        fc <- compileLocal $ compileFun False d
+        Hs.InstDecl _ _ _ (Just fc) <- compileLocal $ compileInstance ToDefinition d
         let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d
         let fc' = {- dropPatterns 1 $ -} replaceName hd uf fc
         reportSDoc "agda2hs.compile.instance" 6 $ vcat $
           text "compileInstanceClause compiled clause: " :
           map (nest 2 . text . pp) fc'
-        return (map (Hs.InsDecl ()) fc', [n])
+        return (fc', [n])
 
        -- Projection of a default implementation: drop while making sure these are drawn from the
        -- same (minimal) dictionary as the primitive fields.
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 1298d224..ab97c950 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -230,7 +230,7 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
   (_, Nothing) -> pure False
   (Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
     DODropped  -> False
-    DOInstance -> False -- not __IMPOSSIBLE__ because of current hacky implementation of `compileInstanceClause`
+    DOInstance -> True
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
index 2ffd550b..dc67796b 100644
--- a/test/AllFailTests.agda
+++ b/test/AllFailTests.agda
@@ -35,3 +35,4 @@ import Fail.PartialCaseNoLambda
 import Fail.NonStarDatatypeIndex
 import Fail.NonCanonicalSpecialFunction
 import Fail.TypeLambda
+import Fail.NonCanonicalSuperclass
diff --git a/test/Fail/NonCanonicalSuperclass.agda b/test/Fail/NonCanonicalSuperclass.agda
new file mode 100644
index 00000000..0fdf807f
--- /dev/null
+++ b/test/Fail/NonCanonicalSuperclass.agda
@@ -0,0 +1,32 @@
+
+module Fail.NonCanonicalSuperclass where
+
+open import Haskell.Prelude
+
+record Class (a : Set) : Set where
+  field
+    foo : a → a
+open Class {{...}} public
+
+{-# COMPILE AGDA2HS Class class #-}
+
+instance
+  ClassBool : Class Bool
+  ClassBool .foo = not
+
+{-# COMPILE AGDA2HS ClassBool #-}
+
+record Subclass (a : Set) : Set where
+  field
+    overlap {{super}} : Class a
+    bar : a
+open Subclass {{...}} public
+
+{-# COMPILE AGDA2HS Subclass class #-}
+
+instance 
+  SubclassBool : Subclass Bool
+  SubclassBool .super = record { foo = id }
+  SubclassBool .bar = False
+
+{-# COMPILE AGDA2HS SubclassBool #-}
diff --git a/test/golden/NonCanonicalSuperclass.err b/test/golden/NonCanonicalSuperclass.err
new file mode 100644
index 00000000..1cc20e94
--- /dev/null
+++ b/test/golden/NonCanonicalSuperclass.err
@@ -0,0 +1,2 @@
+test/Fail/NonCanonicalSuperclass.agda:28,3-15
+illegal instance:  record { foo = id }