Type error message with bad location information

[brianhuffman]

Here's an example source file Test.cry that contains a type error:

module Test where

type RING a =
  { int : Integer -> a
  , mul : a -> a -> a
  }

theRING : {a} Ring a => RING a
theRING =
  { int = fromInteger
  , mul = (*)
  }

w_512 : Z 7681
w_512 = 62

foo : {a} RING a -> a -> [16][16]a -> [16][16]a
foo R w xs = xs

bar : {a} RING a -> a -> [16][16]a -> [16][16]a
bar R w xs = xs

property foo_bar xs =
  foo R w (bar R w xs) == map (R.mul (R.int 256)) xs
  where (R, w) = (theRING, w_512)

When loading this file, cryptol shows the following message:

Loading module Cryptol
Loading module Test

[error] at Test.cry:1:1--21:16:
  Type mismatch:
    Expected type: Z 7681
    Inferred type: [16](Z 7681)
    When checking type of field 'mul'
[error] at Test.cry:1:1--21:16:
  Type mismatch:
    Expected type: Z 7681
    Inferred type: [16](Z 7681)
    When checking type of field 'mul'

The indicated location of the error, 1:1--21:16, is the entire file up to the end of the declaration for bar.

I would expect the error message to instead indicate which expression (or at least which declaration) contains the error.

[brianhuffman]

I noticed that removing the property pragma affects the reported location:

[error] at Test.cry:23:1--25:34:
  Type mismatch:
    Expected type: Z 7681
    Inferred type: [16](Z 7681)
    When checking type of field 'mul'
[error] at Test.cry:23:1--25:34:
  Type mismatch:
    Expected type: Z 7681
    Inferred type: [16](Z 7681)
    When checking type of field 'mul'

The new location is now the entire declaration for foo_bar. It seems that the property pragma screws up the location information on the declaration somehow. Getting this same location even when property is used would probably suffice to close this ticket, although identifying the specific sub-expression would be better. (I suppose we could open a separate ticket for that, as I expect it would require a different fix.)