Internal error when typechecking malformed forall clause

[patrickt]

Here’s a function with more than one constraint, that typechecks fine:

(defn show-equal : (forall [s] (Show s) (Eq s) => {s -> s -> Bool})
  [[a b] { {a == b} && {(show a) == (show b)}}])

I originally messed up the syntax, and thought that forall’s second parameter was a list:

(forall [s] ((Show s) (Eq s)) => {s -> s -> Bool})

When the typechecker tries to inspect this, I get an internal error:

../../../../Applications/Racket v7.0/collects/racket/private/map.rkt:180:2: andmap: all lists must have same size
  first list length: 1
  other list length: 2
  procedure: #<procedure:types-match?!>

[iitalics]

I get a similar but different error. Which commit are you on and which version of Racket are you running?

[patrickt]

@iitalics This is with Racket 7.0 and a Hackett installed from raco pkg, which appears to have targeted f5a080e.

[lexi-lambda]

Here’s what is happening:

1. ((Show s) (Eq s)) is the same as (Show s (Eq s)).

2. The typechecker looks up the information for Show and tries to zip the argument types with the instance type variables.

3. The arity mismatch is never caught, so the typechecker explodes.

The easy fix would be to insert some ad-hoc arity-checking code that complains about the mismatch. The right fix is to implement actual kindchecking, since (Show s (Eq s)) is an ill-kinded type. I’ve been putting kindchecking off for ages, though, since it would take a lot of thought and possibly some serious refactoring, so maybe the quick fix is the right thing for now.