Some position handling issues in the typechecker

[sauclovian-g]

The following file produces five type errors. The real problem is that the Key argument of once is commented out. (When I originally hit this, it was just missing entirely, by accident.)

It would probably be nice if the typechecker had an explicit message for "your function has too many parameters for its type signature", which it doesn't. That's what's really going on.

However, the curious bit is that the first output error is reported with a position starting at line 1, column 1. The ending position, however, appears to be the intended location. It's odd that the position can get spliced like this, and suggests something maybe worth looking into.

I assume this error is getting printed first because the errors get sorted by starting line, so the fact that it's first (which is distracting for the user, since normally if there's a pile of errors the first one is the real issue and the rest are fallout) is a side effect and not its own problem.

Also though, the position of the second error, which is reporting that the return type of once is wrong and reflects the real issue, is reported as the entirety of the function rather than, say, the return value. This is not ideal, especially in a large function.

What's here is cut down from a much larger example so it doesn't mean anything. It's a fold over a list of pairs (has to be a list of tuples to tickle the problem, I think) that updates a newtype.

Bug.cry:

module Bug where

import Array

type Widget = [3]
type Wombat = [4]
type Key = [5]
newtype Info = {
   stuff: Array [5] [6]
}

once: Info -> /*Key ->*/ Widget -> Wombat -> Info
once info key widget wombat = info'
   where
      info' = Info {
         stuff = arrayUpdate info.stuff key 0
      }

iter: {n} n < 10 => Info -> Key -> [n] (Widget, Wombat) -> Info
iter info key entries = infos ! 0
   where
      infos = [info] # [once info' key widget wombat
                           | info' <- infos
                           | (widget, wombat) <- entries]

process: {n} n < 10 => Info -> [n] (Widget, Wombat) -> Info
process info entries = iter info 0 entries

Output (from current head, which is also 3.2.0):

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0.99 (0985325)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Array
Loading module Bug
[error] at Bug.cry:1:1--24:37:
  Type mismatch:
    Expected type: 3
    Inferred type: 4
    Context: [ERROR] _
    When checking type of 0th tuple field
[error] at Bug.cry:13:1--17:8:
  Type mismatch:
    Expected type: Bug::Info
    Inferred type: ?a -> Bug::Info
    When checking type of function result
  where
  ?a is the type of 'wombat' at Bug.cry:13:22--13:28
[error] at Bug.cry:16:41--16:44:
  Type mismatch:
    Expected type: 5
    Inferred type: 3
    Context: [ERROR] _
    When checking type of function argument
[error] at Bug.cry:22:25--22:29:
  Type mismatch:
    Expected type: [4] -> Bug::Info
    Inferred type: Bug::Info
    Context: _ -> _ -> _ -> ERROR
    When checking function call
[error] at Bug.cry:22:36--22:39:
  Type mismatch:
    Expected type: 3
    Inferred type: 5
    Context: [ERROR] _
    When checking type of function argument