Escaped quantified variables

[ramsdell]

$ cryptol bug.tex
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸
version 2.8.0

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: Cryptol.TypeCheck.Monad.extendSubst
Message: Escaped quantified variables:
Substitution: ?front1035 := 2 * k1042 - n891 Vars in scope: [n891]
Escaped: [k`1042]
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.8.0-CNGuMszJOXX2THCqGgAi4I:Cryptol.Utils.Panic
panic, called at src/Cryptol/TypeCheck/Monad.hs:562:16 in cryptol-2.8.0-CNGuMszJOXX2THCqGgAi4I:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------
bug.tex.txt

(The input LaTeX file is ugly. It is from an early step in development, so don't look at its contents too closely.)

[brianhuffman]

Here is a minimized example that generates the same error:

round : {n} (fin n) => [n] -> [n]
round k = output k
  where
    m1 = zero # k

    output : {k} (fin k) => [k] -> [k]
    output mo = m1 ^ mo

[brianhuffman]

I think I understand what's going on here. This is probably a situation where we should be reporting a user error, and not a panic.

In the minimized example I posted, think about what the type checker is doing: When checking the declaration for m1, it invents a unification variable for the type of m1, and it also invents unification variables for the type arguments to the # operator and zero. All of these unification variables are tagged with the set of bound variable names in scope, i.e. {n}. In order for the program to type check, we must ensure that any unification variable is instantiated with a term that only mentions bound type variables that are in scope.

The problem here is that when type checking function output, the body of the declaration causes the unification variable for m1's type (which is marked as being in the scope of only n) to be unified with the type of argument m0, which is the bound variable k. At this point we should report a user type error, as this means that the function output is not as polymorphic as the type signature claims.

To fix this, we need to demote this situation from a panic to an ordinary user type error, and make a better type error message. Perhaps we should look at what ghc does in similar situations.

[yav]

Yep, I think you are exactly right. We actually even have a type error for that, see TypeVarialbeEscaped in Cryptol.TypeCheck.Error, so probably all we have to do is emit one of those.

[ramsdell]

Wow. You guys are fast. Thanks for taking this on so quickly.

[brianhuffman]

Ok, I did some tracing and I discovered that this particular panic message came from a call to extendSubst from function simplifyAllConstraints, which gets its Subst value from function quickSolver in module Cryptol.TypeCheck.Solve. We have a documented invariant for the Subst datatype, and apparently the Subst returned by quickSolver violates it.

We shouldn't actually demote the panic to an error message in extendSubst, as this is checking a datatype invariant that we should never actually be violating anywhere in the program; if we discover that the invariant has been violated then we should panic. Instead we need for the function quickSolver to notice the problem earlier and report it as a user error, much in the same way that the mgu function from Cryptol.TypeCheck.Unify does.

[brianhuffman]

This call to singleSubst in function improveEq (which is in turn called by quickSolver) seems suspect:

cryptol/src/Cryptol/TypeCheck/Solver/Improve.hs

Lines 67 to 70 in 1c38465

	rewrite this other =
	do x <- aTVar this
	guard (considerVar x && x `Set.notMember` fvs other)
	return (singleSubst x other, [])

In particular, the guard condition here is not sufficient to establish the datatype invariant on the Subst value created by singleSubst.

My recommendation would be that we rename singleSubst to something like unsafeSingleSubst or uncheckedSingleSubst, as it does not enforce the Subst datatype invariant. Then we should introduce a new singleSubst function that returns a datatype that explicitly indicates the failure conditions of recursive substitution (which we seem to do a good job of checking for) or bound variable escaping its scope (which we don't).

[brianhuffman]

I have a pull request (#726) that fixes this. Now, when loading bug.tex I get a "Failed to validate user-specified signature" error instead of a panic:

Loading module Cryptol
Loading module Main
[warning] at bug.tex:134:12--134:29:
  Defaulting type argument 'front' of '(Cryptol::#)' to 0
[warning] at bug.tex:132:30--132:38:
  Defaulting type argument 'ix' of '(Cryptol::<<)' to width n`930
  where
  n`930 is signature variable 'n' at bug.tex:128:11--128:12
[warning] at bug.tex:133:38--133:46:
  Defaulting type argument 'a' of 'Cryptol::fromTo' to [width n`930]
  where
  n`930 is signature variable 'n' at bug.tex:128:11--128:12
[error] at bug.tex:138:7--144:43:
  Failed to validate user-specified signature.
    in the definition of 'Main::f', at bug.tex:138:7--138:8,
    we need to show that
      for any type m
      assuming
        • fin m
        • m > 0
      the following constraints hold:
        • m == n`930
            arising from
            matching types
            at bug.tex:139:20--139:23
        • n`930 == m
            arising from
            matching types
            at bug.tex:143:33--143:35
        • 2 * n`930 > 0
            arising from
            use of expression Main::lfsr
            at bug.tex:143:23--143:27
  where
  n`930 is signature variable 'n' at bug.tex:128:11--128:12
[error] at bug.tex:147:7--147:49:
  Failed to validate user-specified signature.
    in the definition of 'Main::output', at bug.tex:147:7--147:13,
    we need to show that
      for any type k
      assuming
        • fin k
        • k > 0
      the following constraints hold:
        • 2 * k >= n`930
            arising from
            matching types
            at bug.tex:147:31--147:49
        • k == n`930
            arising from
            matching types
            at bug.tex:147:31--147:49
  where
  n`930 is signature variable 'n' at bug.tex:128:11--128:12