Do not drop instance clauses but instead check canonicity

This was a regression introduced by #304 that went unnoticed due to a lack of a (failing) test case

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.

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
 

test/AllFailTests.agda

@@ -35,3 +35,4 @@ import Fail.PartialCaseNoLambda
 import Fail.NonStarDatatypeIndex
 import Fail.NonCanonicalSpecialFunction
 import Fail.TypeLambda
+import Fail.NonCanonicalSuperclass

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 #-}

test/golden/NonCanonicalSuperclass.err

@@ -0,0 +1,2 @@
+test/Fail/NonCanonicalSuperclass.agda:28,3-15
+illegal instance:  record { foo = id }