Panic: type cannot be demoted inf - inf

[weaversa]

Help...related to #1693.

f : {m, n} (n < m) => [m] -> [n]
f x = take x

Cryptol> f (zero : [inf]) : [inf]
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:  [Eval] evalTF
  Message:   type cannot be demoted
             inf - inf
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.1.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:244:25 in cryptol-3.1.0.99-inplace:Cryptol.Eval.Type
%< ---------------------------------------------------

[weaversa]

take outside of a function seems to work just fine.

Cryptol> take (zero : [inf]) : [inf]
[False, False, False, False, False, ...]

[yav]

This is due to an incorrect simplification rule: a = ?x + b ~> ?x = a - b. This is only valid when b is finite, but this additional check was missing. PR #1697 fixes this, and under this PR the original definition of f is rejected, because there is no way to infer the back argument to pass to take.

[yav]

I am looking into why take is working on its own. I suspect it is either another incorrect rule or, perhaps, we are somehow defaulting the back argument to 0.