where/error doesn't report errors sometimes

[nikomatsakis]

I had this function:

(define-metafunction formality-logic
  ;; Extend `Env` with a single variable declared in the given universe with the given quantifier.
  env-with-var : Env VarId ParameterKind Quantifier Universe -> Env

  [(env-with-var Env VarId ParameterKind Quantifier Universe)
   (Hook Universe ((VarId ParameterKind Quantifier Universe) VarBinder ...) Substitution VarInequalities Hypotheses)
   (where/error (Hook Universe (VarBinder ...) Substitution VarInequalities Hypotheses) Env)
   ]
  )

and I was, quite confusingly, getting errors like this:

env-with-var: no clauses matched for (env-with-var ((Hook: #<formality-ty-hook>) (UniverseId 2) ((X«2» TyKind ForAll (UniverseId 2)) (A«0» TyKind ForAll (UniverseId 1)) (B«1» TyKind ForAll (UniverseId 1))) () ((() <= X«2» <= (B«1» A«0»))) ()) X«2»1 TyKind Exists (UniverseId 1))

This was true despite the fact that I could clearly see that redex was entering the function, and there seems to be no possible way for the first clause to be rejected (it has where/error, after all).

It turned out that the problem was that I was using the term Universe more than once.

[rfindler]

I think I get what you're saying, but do you think you could make a standalone example just to make sure I'm getting it right?

[nikomatsakis]

Yes. I was just too lazy and wanted to file the issue before I forgot the problem. I'll circle back to it.

[nikomatsakis]

Standalone example:

#lang racket
(require redex/reduction-semantics)

(define-language issue-254
  (Id ::= variable-not-otherwise-mentioned)
  )

(define-metafunction issue-254
  test-function : Id Id -> boolean

  [(test-function Id_1 Id)
   #t
   (where/error Id Id_1)
   ]
  )

(pretty-print (term (test-function Foo Bar)))

Running this yields:

> racket -l errortrace -l racket/base -e '(require "src/issue254.rkt")' 
test-function: no clauses matched for (test-function Foo Bar)
  errortrace...:
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:20: (test-function Foo Bar)
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:14: (term (test-function Foo Bar))
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:0: (pretty-print (term (test-function Foo Bar)))
  context...:
   /home/nmatsakis/stow/racket/share/pkgs/redex-lib/redex/private/error.rkt:10:0: redex-error
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:0
   body of "/home/nmatsakis/versioned/mir-formality/src/issue254.rkt"
   body of top-level

but I expect to see "define-metafunction: where/error did not match"

[rfindler]

@shhyou it looks like there is an explicit test case checking for something very close to this situation that disagrees with this issue.

Here's the commit and here's the relevant test case.

I am currently disagreeing with the existing test case and have put a candidate commit on a branch. There are a bunch of details in the commit because #f can come out for a lack of a match and also because the clause returns #f so that's why the extra thunk was introduced.

Anyway, what do you think?

[shhyou]

I don't really get the fix, so let me ask this instead. Does the fix distinguish between these three situations?

1. Match failure in where/error because the shape of the pattern doesn't match
2. Match failure in where/error because repeated names are assigned non-equal values
3. Match failure in other where clauses that come after where/error in the same metafunction case

It looks like the existing code conflated case 2 and 3, which I suppose is wrong.

[rfindler]

I think it does!

I think the third case is separated from the second case because it goes through a different code path; a where/error ends up in the helper function combine-where/error-results and a where (no /error) ends up in combine-where-results/flatten. (I had to change that path, but only because I changed the shape of the code that the macro generates that's in common to the two paths.)

Do you have an idea for a new test case maybe?

[shhyou]

Here is an attempt of case 2. I am not sure if this will take a different path from the test case at line 708--716.

(define-metafunction empty-language
  [(f integer)
   0
   (where/error integer 3)
   (where #t #t)]
  [(f _) 1])

(with-handlers ([exn:fail? exn-message])
  (term (f 4))) ;; => #rx"where/error"

Here is an attempt of case 3:

(define-metafunction empty-language
  [(h integer)
   0
   (where/error integer 3)
   (where integer 4)]
  [(h _) 1])

(term (h 3)) ;; => should be 1
(with-handlers ([exn:fail? exn-message])
  (term (h 4))) ;; => #rx"where/error"

[rfindler]

Thanks! I think the test case probably should be changed. If you think there is more to worry about or I'm missing something, then please let me know!