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

[fabianhjr]

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

[gallais]

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

[fabianhjr]

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.

[fabianhjr]

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