search

edwinb / Idris2-boot

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

Proof search produces ill-typed terms #355

Open ziman opened 4 years ago

ziman commented 4 years ago

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.