Panic when resolving type fixities

[ghost]

In a type such as f : {m, n, k} (n == max 2 m, k == m + 1) => [m] -> [k][n], if I were to accidentally omit the comma in the constraints as so:

f : {m, n, k} (n == max 2 m k == m + 1) => [m] -> [k][n]
f x = zero

Cryptol will crash instead of reporting a parse error or malformed type:

$ cryptol-2.7.0-CentOS7-64/bin/cryptol
version 2.7.0

Loading module Cryptol
Cryptol> :l bug.cry
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  Renamer
  Message:   fixity problem for type operators
             TApp (PC PEqual) [TApp (PC PEqual) [TUser (UnQual (Ident False "n")) [],TLocated (TUser (UnQual (Ident False "max")) [TLocated (TNum 2) (Range {from = Position {line = 1, col = 25}, to = Position {line = 1, col = 26}, source = "./bug.cry"}),TLocated (TUser (UnQual (Ident False "m")) []) (Range {from = Position {line = 1, col = 27}, to = Position {line = 1, col = 28}, source = "./bug.cry"}),TLocated (TUser (UnQual (Ident False "k")) []) (Range {from = Position {line = 1, col = 29}, to = Position {line = 1, col = 30}, source = "./bug.cry"})]) (Range {from = Position {line = 1, col = 21}, to = Position {line = 1, col = 30}, source = "./bug.cry"})],TLocated (TUser (UnQual (Ident False "m")) []) (Range {from = Position {line = 1, col = 34}, to = Position {line = 1, col = 35}, source = "./bug.cry"})]
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/Renamer.hs:687:18 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.ModuleSystem.Renamer
%< --------------------------------------------------- 

[brianhuffman]

Here's a minimized example:

g : {i} (i == i == i) => [i]
g = zero

Writing i >= i >= i also causes a panic. I guess the problem is that the code expects to always be able to resolve the associativity of the infix type operators one way or the other, but == and >= are both defined to be non-associative.

[brianhuffman]

The source of the problem is the call to panic in the renamer code: https://github.com/GaloisInc/cryptol/blob/master/src/Cryptol/ModuleSystem/Renamer.hs#L693

The comment there, "it's a real error if the fixities didn't work out" is just wrong. If we have any operators to have non-associative fixities, there will always be the possibility of users chaining them together like i == i == i, so we shouldn't panic. Instead we should record a user error to report later.

I was thinking of replacing the call to panic with something like record (FixityError o1 o2) (as is done when an expression-level fixity error occurs) but at that point in the code we don't have the names and location information available. We should reorganize the code so that parsing infix types works more similarly to parsing infix expressions.

[brianhuffman]

The link to the source code in the previous post is broken; here's a new permalink to a current version:

cryptol/src/Cryptol/ModuleSystem/Renamer.hs

Lines 640 to 643 in 67fc367

	-- As the fixity table is known, and this is a case where the fixity came
	-- from that table, it's a real error if the fixities didn't work out.
	FCError -> panic "Renamer" [ "fixity problem for type operators"
	, show (o2 t z) ]