Multiple constrains with unreseolved type parameters on interface declaration cause typecheck issue

[edwinb]

Issue by fabianhjr
Tuesday Apr 21, 2020 at 20:32 GMT
Originally opened as edwinb/Idris2-boot#306

---

Steps to Reproduce

module Test

interface Interface1 a where
  x : Bool

interface Interface2 a where
  y : Bool

interface (Interface1 a, Interface2 a) => InterfaceMix a where
  z : Bool
  z = x || y 

Expected Behavior

Typecheck

Observed Behavior

Test.idr:11:7--11:9:While processing right hand side of Default implementation of z at Test.idr:11:3--13:1:
Can't find an implementation for Interface1 ?a

[edwinb]

Comment by gallais
Tuesday Apr 21, 2020 at 20:56 GMT

---

Isn't the problem under-constrained?
There is no way to infer a from the type x ought to have.

[edwinb]

Comment by fabianhjr
Tuesday Apr 21, 2020 at 20:59 GMT

---

I extracted this from some testing I am doing with Bools and Group interfaces,

module Algebra.Group.Commutative

import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import Algebra.Group.Group

%default total

public export
interface Magma a ⇒ CommutativeMagma a where
  proofOfCommutativity : (x, y: a) → x `op` y = y `op` x

public export
interface (CommutativeMagma a, Semigroup a) => CommutativeSemigroup a where

public export
interface (CommutativeMagma a, Monoid a) => CommutativeMonoid a where

public export
interface (CommutativeMagma a, Group a) => CommutativeGroup a where

{-
-- TODO: Uncomment when Idris2!306 gets fixed
(CommutativeMagma a, Semigroup a) => CommutativeSemigroup a where
(CommutativeMagma a, Monoid a) => CommutativeMonoid a where
(CommutativeMagma a, Group a) => CommutativeGroup a where
-}

So the idea is that from:

[BoolSumMagma] Magma Bool where
  False `op` False = False
  _     `op` _     = True

[BoolSumCommutativeMagma] CommutativeMagma Bool using BoolSumMagma where
  proofOfCommutativity False False = Refl
  proofOfCommutativity False True  = Refl
  proofOfCommutativity True  False = Refl
  proofOfCommutativity True  True  = Refl

The implementations of CommutativeSemigroup and CommutativeMonoid get derived.

Since it was the same error message when reduced to the one on the first message I left it as reduced as possible.

[edwinb]

Comment by fabianhjr
Tuesday Apr 21, 2020 at 21:25 GMT

---

Oh, wait I get what you are refering to now.

module Test

interface Interface1 a where
  x : a

interface Interface2 a where
  y : a

interface (Interface1 a, Interface2 a) => InterfaceMix a where
  op : a -> a -> a
  z : a
  z = x `op` y 

This works and is less hacky

[gallais]

I still believe that the original problem was under-constrained
and thus working as expected.