Panic: type variable not bound

[brianhuffman]

A recursive declaration with a pattern binding causes Cryptol to panic. The same thing happens with let at the repl, or putting (x, y) = (y, x) in a file.

Cryptol> let (x, y) = (y, x)
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  f4ce1a46f0705753d7218b5c89839e32aa2219ed
  Branch:    master (uncommited files present)
  Location:  [Eval] evalType
  Message:   type variable not bound
             TVFree 859 KType (fromList []) (TVarInfo {tvarSource = Range {from = Position {line = 1, col = 5}, to = Position {line = 1, col = 20}, source = "<interactive>"}, tvarDesc = DefinitionOf (Name {nUnique = 4546, nInfo = Declared (ModName "<interactive>"), nIdent = Ident False "x", nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 6}, to = Position {line = 1, col = 7}, source = "<interactive>"}})})
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Monad.hs:186:17 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:90:20 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Type
  evalType, called at src/Cryptol/Eval/Type.hs:119:8 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Type
  evalValType, called at src/Cryptol/Eval.hs:252:10 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval
%< ---------------------------------------------------

[brianhuffman]

Here's the output when you turn on debugging:

Cryptol> :set debug=yes, please
Cryptol> let (x, y) = (y, x)
/* Recursive */
<interactive>::y : ?<interactive>::x`859
<interactive>::y = (<interactive>::__p0 <interactive>::x`859) .1 /* of 2 */
<interactive>::x : Bit
<interactive>::x = (<interactive>::__p0 <interactive>::x`859) .0 /* of 2 */
<interactive>::__p0 : {a} (a, a)
<interactive>::__p0 = \{a} -> (<interactive>::y, <interactive>::x)

cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
[...]

[brianhuffman]

Here's another variant where the panic doesn't happen right away:

Cryptol> let (x, y) = (x, y)
Cryptol> :t x
x : Bit
Cryptol> :t y
y : Bit
Cryptol> x
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  f4ce1a46f0705753d7218b5c89839e32aa2219ed
  Branch:    master (uncommited files present)
  Location:  [Eval] evalType
  Message:   type variable not bound
             TVBound (TParam {tpUnique = 863, tpKind = KType, tpFlav = TPOther Nothing, tpInfo = TVarInfo {tvarSource = Range {from = Position {line = 1, col = 5}, to = Position {line = 1, col = 20}, source = "<interactive>"}, tvarDesc = DefinitionOf (Name {nUnique = 4549, nInfo = Declared (ModName "<interactive>"), nIdent = Ident False "y", nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 9}, to = Position {line = 1, col = 10}, source = "<interactive>"}})}})
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Monad.hs:186:17 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:90:20 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Type
  evalType, called at src/Cryptol/Eval/Type.hs:119:8 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval.Type
  evalValType, called at src/Cryptol/Eval.hs:134:28 in cryptol-2.5.0-KseLOOjkIOa7MXdDpk4N3H:Cryptol.Eval
%< ---------------------------------------------------

[yav]

Actually, the binding doesn't even need to be recursive. The problem is really with all top-level pattern bindings, if some the types are not inferred (i.e. could be generalized). For example:

a : {a} a
a = a

(x,y) = (a,a)

I know what's wrong here, so I'll have a go at fixing it.

[yav]

Reopening, as there is another issue related to rechursive bindings. I am working on fixing it