search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.44k stars 644 forks source link

Idris having issue with nested auto implicits #4735

Open Sintrastes opened 5 years ago

Sintrastes commented 5 years ago

Note: This was originally a question on stack exchange, but I got no response there, and this seems like it has a good chance of being a bug with Idris itself, so I figured I would post it as an issue here.

I'm writing an interface for partial monoids as follows:

infixr 9 <>
interface PartialMonoid (m : Type) where
     compatible : m -> m -> Bool
    (<>) : (a : m) -> (b : m) -> {auto p : compatible a b = True} -> m

With a simple implementation as proof of concept:

data MyPos : Type where
   A : MyPos
   B : MyPos
   C : MyPos

op : (a : MyPos) -> (b : MyPos) -> Bool
op A A = True
op B B = True
op C C = True
op A B = True
op B A = True
op A C = True
op C A = True
op x y = False

PartialMonoid MyPos where
   compatible = op
   A <> A = A
   B <> B = B
   C <> C = C
   A <> B = B
   A <> C = C
   C <> A = C
   B <> A = B
   (<>) B C {p = Refl} impossible
   (<>) C B {p = Refl} impossible

Whenever I try to evaluate something like A <> B in the REPL, I get the expected behavior. However, when evaluating (for instance) (A <> B) <> A, instead of the expected B, I get 

Type mismatch between
            MyPos (Type of A)
    and
            compatible A B = True (Expected type)

This is confusing to me, because if in the REPL I do:

:let x = (A <> B)
x <> A

then I get the expected B.

I should also note that this seems to be an issue with how Idris' interface/implementation mechanism handles implicits. I get the expected behavior If I'm using some other operator (say <..>) defined normally (i.e. not as the instance of an interface).

jfdm commented 5 years ago

@Sintrastes I had a quick play with your code a managed to get a working solution, the code is at the end. Essentially, I made the auto implicit an explicit argument, and remove a possible implicit misidentification by the compiler (capitalised compatible).

Thus the follow 'works'.

λΠ> (A <> B $ Refl) <> A $ Refl

The following is wrong, but I shall leave it here for posterity: I think what is happening here is that Idris is having trouble finding the proof as your operator is Right Associative. When nesting you are asking it to find something it doesn't have the information for. In this case, I believe this will be 'expected behaviour'.

I believe, the reason that Idris is not finding the proof is that it doesn't have the information required. I get incomplete term when performing nested operations. I am not sure this is correct, but I am not too sure. I'll look at this in detail later, if I have time.

Again wrong. We can rewrite your code to ensure Idris does find the nested proof by making the operator left associative. I have a local working version that does work. But I made more changes.

I have a different version of the code, locally, that follows some good design patterns when working with Idris code and proving things.

  1. I made the interface explicit and operator-less.
  2. Added an operator in which the auto proof is constructed using an auto implicit. Complete with using the interface to specify the explicit proof required.
  3. I turned your proofs of equality into predicates (data) to remove the need to explicitly state failing cases.

I am not going to provide my entire local version, as it might be a good exercise to complete for you to get your teeth into. My interface is at the very end.

I hope this helps.

infixr 9 <>
interface PartialMonoid (m : Type) where
     Compatible : m -> m -> Bool
     (<>) : (a : m) -> (b : m) -> (Compatible a b = True) -> m

data MyPos : Type where
   A : MyPos
   B : MyPos
   C : MyPos

op : (a : MyPos) -> (b : MyPos) -> Bool
op A A = True
op B B = True
op C C = True
op A B = True
op B A = True
op A C = True
op C A = True
op x y = False

PartialMonoid MyPos where
   Compatible = op
   (<>) A A (Refl) = A
   (<>) B B (Refl) = B
   (<>) C C (Refl) = C
   (<>) A B (Refl) = B
   (<>) A C (Refl) = C
   (<>) C A (Refl) = C
   (<>) B A (Refl) = B
   (<>) B C (Refl) impossible
   (<>) C B (Refl) impossible

Hint Hint

infixl 9 <>
interface PartialMonoid (m : Type) where
     data Compatible : m -> m -> Type
     merge : (a : m) -> (b : m) -> (Compatible a b) -> m
Sintrastes commented 5 years ago

@jfdm Thank you for your suggestions and taking a look at this issue. Unfortunately, I still run into the same issue when following your suggestions (maybe there is still something I'm doing differently?)

interface PartialMonoid (m : Type) where
     data Compatible : m -> m -> Type
     merge : (a : m) -> (b : m) -> (Compatible a b) -> m

data MyPos : Type where
   A : MyPos
   B : MyPos
   C : MyPos

data MyPosCompat : MyPos -> MyPos -> Type where
  MyRefl   : (a : MyPos) -> MyPosCompat a a
  CompatAB : MyPosCompat A B
  CompatBA : MyPosCompat B A
  CompatAC : MyPosCompat A C
  CompatCA : MyPosCompat C A

myMerge : (a : MyPos) -> (b : MyPos) -> (p : MyPosCompat a b) -> MyPos
myMerge A A (MyRefl A) = A
myMerge B B (MyRefl B) = B
myMerge C C (MyRefl C) = C
myMerge A B CompatAB = B
myMerge B A CompatBA = B
myMerge A C CompatAC = C
myMerge C A CompatCA = C
myMerge B C (MyRefl x) impossible
myMerge C B (MyRefl x) impossible

PartialMonoid MyPos where
  Compatible = MyPosCompat
  merge = myMerge

-- The following operator works as intended
infixl 9 <.>
(<.>) : (a : MyPos) -> (b : MyPos) -> {auto p : MyPosCompat a b} -> MyPos
(<.>) a b {p=p} = myMerge a b p 

-- The following operator still does not work
infixl 9 <>
(<>) : PartialMonoid m => (a : m) -> (b : m) -> {auto p : Compatible a b} -> m
(<>) a b {p=p} = merge a b p

I am still bewildered as to why writing an operator specifically for MyPos works as intended, but the generic <> operator gives me incomplete term errors. This seems to me like an issue with the interface/instance mechanism in Idris, and how it interacts with implicits.