Simple mistake leads to moral crushing error message

[weaversa]

So, we're teaching a class on Cryptol. One of the students writes the following:

WStep:
    {n}
    (fin n, n >= 2) ->
    ([128] -> [128]) -> [n][64] -> [64] -> [n][64]
WStep CIPHk ([A] # Rs) t = [A'] # Rs'
  where
    [MSB, LSB] = split (CIPHk (A # head Rs))
    A'         = MSB ^ t
    Rs'        = tail Rs # [LSB]

Which produces this when read into Cryptol:

Loading module Cryptol
Loading module Main
[warning] at bugs.cry:7:36--7:40:
  Defaulting type argument 'n' of 'head' to 0

[error] at bugs.cry:1:1--5:22:
  Type mismatch:
    Expected type: [2][n`910][64]
    Inferred type: [128] -> [128]
  where
  n`910 is signature variable 'n' at bugs.cry:2:6--2:7
[error] at bugs.cry:3:6--3:11:
  Incorrect type form.
    Expected: a value type
    Inferred: a constraint
[error] at bugs.cry:3:13--3:19:
  Incorrect type form.
    Expected: a value type
    Inferred: a constraint
[error] at bugs.cry:5:1--9:33:
  Failed to validate user-specified signature.
    in the definition of 'WStep', at bugs.cry:5:1--5:6,
    we need to show that
      for any type n
      the following constraints hold:
	• fin n
            arising from
            use of expression (#)
            at bugs.cry:7:32--7:43
[error] at bugs.cry:5:28--5:38:
  Type mismatch:
    Expected type: [64] -> [n`910][64]
    Inferred type: [2][n`910][64]
  where
  n`910 is signature variable 'n' at bugs.cry:2:6--2:7
[error] at bugs.cry:7:25--7:30:
  Type mismatch:
    Expected type: [2 * n`910][64] -> [2 * n`910][64]
    Inferred type: (?err, ?err)
  where
  ?err is type error place-holder at bugs.cry:3:6--3:11
  ?err is type error place-holder at bugs.cry:3:13--3:19
  n`910 is signature variable 'n' at bugs.cry:2:6--2:7

I'm pretty sure this is the error message that most closely relates to the actual bug:

  Incorrect type form.
    Expected: a value type
    Inferred: a constraint

But even that doesn't tell the student what he did wrong.

[robdockins]

In an ideal world, what would you like to see here? It might be possible to add a hint about using the wrong arrow to the Incorrect type form message. Figuring out how issue better error messages with "misaligned" argument types is pretty tricky.

[weaversa]

Have you used Clang? It has this really cool "Did you mean?" thing it does with errors.

Following their error handling, In an ideal world I would l see:

[Error] something on line something something
Did you mean '(fin n, n >= 2) =>'

The arrow is bolded...GitHub needs colors!

[weaversa]

@robdockins...I know you've used Clang.

[yav]

We already have some code to prioritize type errors, so maybe we should add a case where kind errors disable all other type errors, I think it is reasonable to make people fix the kind errors before we show them other stuff.

As for the "did you mean part", I think to get that to work, we'd have to remember the context in which the kind error occurred, (e.g., checking a user signature), which we currently don't, but shouldn't be hard to do.

[weaversa]

I think it is reasonable to make people fix the kind errors before we show them other stuff.

You know what would be really cool? If the "did you mean" part works, after the kind errors, the rest of the checking could be predicated on assuming that you did actually mean those things. I imagine you would get much more relevant error messages.

[brianhuffman]

We were thinking of having Cryptol show only kind error messages when there is a kind error, and not show a bunch of type error messages in that case.

[yav]

Should be fixed by MR #908