Using /^ operator doesn't generate proof obligations like it should

[brianhuffman]

The following declaration fails to type check, because we have tried to use i - j without being able to prove i >= j or fin j.

foo : {i, j} [i - j]
foo = zero

This other declaration should fail for similar reasons, but the typechecker accepts it.

foo : {i, j} [i /^ j]
foo = zero

According to the semantics of /^ (as specified in Cryptol.TypeCheck.Solver.InfNat) i /^ j should only be defined if we can prove fin i, fin j, and j >= 1. Every use of /^ should produce these proof obligations.

[brianhuffman]

This problem can also lead to a panic:

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

%< ---------------------------------------------------
  Revision:  a336d76f7fb6fe202af6c47c2c8f8e2221468f99
  Branch:    master (uncommited files present)
  Location:  [Eval] evalType
  Message:   Lingering typer error
             (error: Invalid type: 1 /^ 0)
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.6.1-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Monad.hs:186:17 in cryptol-2.6.1-inplace:Cryptol.Eval.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:110:28 in cryptol-2.6.1-inplace:Cryptol.Eval.Type
  evalType, called at src/Cryptol/Eval/Type.hs:126:8 in cryptol-2.6.1-inplace:Cryptol.Eval.Type
  evalNumType, called at src/Cryptol/Eval/Type.hs:114:11 in cryptol-2.6.1-inplace:Cryptol.Eval.Type
  evalType, called at src/Cryptol/Eval/Type.hs:119:8 in cryptol-2.6.1-inplace:Cryptol.Eval.Type
  evalValType, called at src/Cryptol/Eval.hs:141:28 in cryptol-2.6.1-inplace:Cryptol.Eval
%< ---------------------------------------------------