edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Ambigous Implementations when using `using` on a constrainted interface implementation #307

Open fabianhjr opened 4 years ago

fabianhjr commented 4 years ago

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