Proof search produces ill-typed terms

[edwinb]

Issue by ziman
Wednesday May 06, 2020 at 20:03 GMT
Originally opened as edwinb/Idris2-boot#355

---

Steps to Reproduce

import Data.Vect

%default total

data Number = N1 | N2 | N3 | N4

Eq Number where
  N1 == N1 = True
  N2 == N2 = True
  N3 == N3 = True
  N4 == N4 = True
  _ == _ = False

namespace All
  public export
  data All : (p : a -> Type) -> (xs : Vect n a) -> Type where
    Nil : All p []
    (::) : {x : a} -> p x -> All p xs -> All p (x :: xs)

namespace AllDifferent
  public export
  data AllDifferent : Vect n Number -> Type where
    Nil : AllDifferent []
    (::) :
        All (\y => x == y = False) xs
        -> AllDifferent xs
        -> AllDifferent (x :: xs)

bug : AllDifferent [N1, N1, N1]
bug = %search

Expected Behavior

%search fails to find the value

Observed Behavior

$ rm -rf build
$ idris2 --debug-elab-check bug.idr
Welcome to Idris 2.  Enjoy yourself!
1/1: Building bug (bug.idr)
Main> :t bug
Main.bug : AllDifferent [N1, N1, N1]
Main> bug
[[Refl, Refl], [Refl], []]

When I lift the lambda from the definition of AllDifferent.(::), the program is correctly rejected.

[edwinb]

This is rejected now, so I'll close.