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 }