Ambigous Implementations when using using on a constrainted interface implementation

[edwinb]

Issue by fabianhjr
Wednesday Apr 22, 2020 at 01:23 GMT
Originally opened as edwinb/Idris2-boot#307

---

Steps to Reproduce

module Test

interface Simple a where
  op : a -> a -> a

interface Simple a => Constraint a where
  square : a -> a
  square x = x `op` x  

-- And
[NamedSimple1] Simple Bool where
  op True True = True
  op _    _    = False

-- Or
[NamedSimple2] Simple Bool where
  op False False = False
  op _     _     = True

[Constrainted1] Constraint Bool using NamedSimple1 where
[Constrainted2] Constraint Bool using NamedSimple2 where

Expected Behavior

Should typecheck and use their corresponding implementations

Observed Behavior

Test.idr:21:1--23:1:While processing right hand side of Constrainted2 at Test.idr:21:1--23:1:
Multiple solutions found in search. Possible correct results:
	NamedSimple1
	NamedSimple2

[gallais]

This is now successfully accepted. \o/