`redex-check #:satsifying` not self-consistent; related to binding?

[wilbowma]

I don't even know what to make of this.

#lang racket

(require redex/reduction-semantics)

(define-language Boxy
  (e ::= x (λ (x : t) e) (e e))
  (t ::= nat (→ t t))
  (x u ::= variable-not-otherwise-mentioned)

  (Γ ::= · (x : t Γ))

  #:binding-forms
  (λ (x : t) e #:refers-to x))

(define-judgment-form
  Boxy
  #:mode (type I I O)
  #:contract (type  Γ e t)

  [---------------------
   (type  (x : t Γ) x t)]

  [(type  Γ x_1 t_1)
   ------------------------------------
   (type  ((name x_2 x_!_1) : t_2 Γ) (name x_1 x_!_1) t_1)]

  [(type  (x : t_1 Γ) e t_2)
   -----------------------------------
   (type  Γ (λ (x : t_1) e) (→ t_1 t_2))]

  [(type  Γ e_1 (→ t_1 t_2))
   (type  Γ e_2 t_1)
   -------------------------
   (type  Γ (e_1 e_2) t_2)])

(module+ test
  (require rackunit)
  #|
  counterexample found after 20 attempts:
  (type
   (y : (→ (→ (→ (→ nat nat) nat) (→ (→ nat nat) nat)) nat) (y : (→ nat nat) ·))
   (((λ (e : (→ nat nat)) e) y)
    ((λ (C : nat) C) (y (λ (H : (→ (→ nat nat) nat)) H))))
   nat)
  |#
  (redex-check
   Boxy
   #:satisfying (type  Γ e nat)
   (judgment-holds (type  Γ e nat))))

[rfindler]

This also demonstrates the bug. Maybe something to do with _!_ patterns.

It seems to require three entries in the environment. Seems like a clue.

#lang racket

(require redex/reduction-semantics)

(define-language Boxy
  (t ::= nat bool)
  (x u ::= variable-not-otherwise-mentioned)
  (Γ ::= · (x : t Γ)))

(define-judgment-form
  Boxy
  #:mode (type I I O)
  #:contract (type Γ x t)

  [---------------------
   (type (x : t Γ) x t)]

  [(type Γ x_1 t_1)
   ------------------------------------
   (type ((name x_2 x_!_1) : t_2 Γ) (name x_1 x_!_1) t_1)])

(define gen (generate-term Boxy #:satisfying (type Γ e nat)))

(define failure #f)

(for ([x (in-range 1000)])
  (define d (gen 4))
  (when d
    (match d
      [`(,_ ,Γ ,e nat)
       (unless (judgment-holds (type ,Γ ,e nat))
         (when (or (not failure)
                   (< (string-length (~s (list Γ e)))
                      (string-length (~s failure))))
           (set! failure (list Γ e))))])))

failure

[rfindler]

Oh, and in case this wasn't obvious, @wilbowma , I think that using a different metafunction is a workaround, something like this. (That is, the unifier inside Redex that finds counterexamples has the capability to track "not equals to" constraints but something seems to be going wrong with the way it gets used in your model).

(define-judgment-form
  Boxy
  #:mode (type I I O)
  #:contract (type Γ x t)

  [---------------------
   (type (x : t Γ) x t)]

  [(type Γ x_1 t_1) (where #t (different x_1 x_2))
   -----------------------------------------------
   (type (x_2 : t_2 Γ) x_1 t_1)])

(define-metafunction Boxy
  different : x x -> boolean
  [(different x x) #f]
  [(different x u) #t])

[wilbowma]

I replaced bang patterns by different in my development, and am still getting the bug. I'm having a hard time shrinking it, but it seems to be related to shadowing. All the examples have the same name bound in the environment, and bound in a term. I'll post the development later if I'm still unsuccessful at shrinking it.

[rfindler]

Maybe there are multiple bugs and I simplified to a different one! Whee. :)

[wilbowma]

This is the smallest I managed to get it. I started from your small examples and added features from mine until it failed.

Working with the box modality, lots of weird things happens in the context.

#lang racket

(require redex/reduction-semantics)

(define-language Boxy
  (t ::= nat bool (→ t t) (□ t))
  (e ::= x (λ (x : t) e) (e e) (box e))
  (x u ::= variable-not-otherwise-mentioned)
  (Γ Δ ::= · (x : t Γ))

  #:binding-forms
  (λ (x : t) e #:refers-to x))

(define-judgment-form
  Boxy
  #:mode (type I I I O)
  #:contract (type Δ Γ e t)

  [---------------------
   (type Δ (x : t Γ) x t)]

  [(type Δ Γ x_1 t_1)
   (where #t (different x_1 x_2))
   ------------------------------------
   (type Δ (x_2 : t_2 Γ) x_1 t_1)]

  [------------------------------------
   (type (x_1 : t_1 Δ) · x_1 t_1)]

  [(type Δ · x_1 t_1)
   (where #t (different x_1 x_2))
   ------------------------------------
   (type (x_2 : t_2 Δ) · x_1 t_1)]

  [(type Δ (x : t_1 Γ) e t_2)
   ------------------------------------
   (type Δ Γ (λ (x : t_1) e) (→ t_1 t_2))]

  [(type Δ Γ e_1 (→ t_1 t_2))
   (type Δ Γ e_2 t_1)
   ------------------------------------
   (type Δ Γ (e_1 e_2) t_2)]

  [(type Δ · e t)
   ------------------------------------
   (type Δ Γ (box e) (□ t))])

#|
counterexample found after 68 attempts:
(type
 (u : bool ·)
 (Y : (→ (→ bool (□ bool)) nat) ·)
 (((λ (R : (→ nat nat)) R) (λ (d : nat) d)) (Y (λ (u : bool) (box u))))
 nat) 
|#
(redex-check
 Boxy
 #:satisfying (type Δ Γ e nat)
 (judgment-holds (type Δ Γ e nat)))

[bfetscher]

Hi there! Finally getting around to taking a look at this...

I think there are indeed two issues. Looks like the original issue does indeed have to do with binding and not mismatches. When I remove the#:binding-forms part of the grammar from the reduced example it passes. This one is actually not a surprise, since the #:satisfying generator doesn't know anything about bindings. And it looks like the generated counterexample doesn't seem to be excluded by the type system itself but the binding as I read it, since the box rule drops Γ from the context.

Probably not solvable by adding a notion of binding to the generator in the short term :) Disallowing grammars with binding seems like going too far. Perhaps an update to the docs for now?

The second one looks like a real issue with _!_ patterns. When the unifier isn't required to walk an entire term disequalities that might be embedded aren't picked up.

Looking into fixes for number 2.