Sequence length type errors can look like errors in sequence member values

[bboston7]

Take the following example:

Cryptol> [[1,2,3], [4,5]]                                                       
                                                                                
[error] at <interactive>:1:11--1:16:                                            
  Type mismatch:                                                                
    Expected type: 3                                                            
    Inferred type: 2                                                            

On first glance, one might assume that a numeric member of one of the sub-sequences was illegal (expected a 3 but found a 2), rather than that the second sequence was too small. It might be clearer to have the types (at least when printed) be something like Integer[3] or even Integer sequence of length 3.

[brianhuffman]

This error message might be nicer if we could provide some context to the numeric types that show up in the message, for example something like this:

[error] at <interactive>:1:11--1:16:
  Type mismatch:
    Expected type: 3 (length of list expression [1,2,3])
    Inferred type: 2 (length of list expression [4,5])

I know that we have a way of annotating type variables with information about where they came from, but I'm not sure if we can do anything like that for concrete types like 2 or 3.

Another idea is that maybe we could say something a bit more specific than just "Type mismatch". The type checker could remember that this particular type equation it's trying to solve came from unifying the types of two elements of the same list, and customize the message accordingly.

[error] at <interactive>:1:11--1:16:
  Type mismatch between list elements:

I also like @bboston7's idea of showing the whole type that failed to match, instead of just the smallest part:

[error] at <interactive>:1:11--1:16:
  Type mismatch:
    Expected type: [3]Integer
    Inferred type: [2]Integer

If we go this route it would be helpful to have some way to highlight the mismatched part of each type; this would be especially important when the types are big.

[error] at <interactive>:1:11--1:16:
  Type mismatch:
    Expected type: [3]Integer
                    ^
    Inferred type: [2]Integer
                    ^

[yav]

The situation should be improved by MR #908