Better error messages when instantiating a module

[yav]

This example is in the context of cryptol-specs (6c6f91e2a9e7f4a9f95d016db0784f875df12ddc)

shell> cryptol ./Primitive/Asymmetric/Signature/DSA/p1024_sha1.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99 (c0ff727)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Common::utils
Loading module Primitive::Keyless::Hash::SHA1
Loading module `where` argument of Primitive::Asymmetric::Signature::DSA::p1024_sha1
Loading module Common::bv
Loading module Common::mod_arith
Loading interface module `parameter` interface of Primitive::Asymmetric::Signature::DSA::DSA
Loading module Primitive::Asymmetric::Signature::DSA::DSA
Loading module Primitive::Asymmetric::Signature::DSA::p1024_sha1
[error] at Primitive/Asymmetric/Signature/DSA/p1024_sha1.cry:1:8--1:57:
  • Unsolvable constraint:
      1024 == 2048
        arising from
        module instantiation
        at Primitive/Asymmetric/Signature/DSA/p1024_sha1.cry:1:8--1:57
[error] at Primitive/Asymmetric/Signature/DSA/p1024_sha1.cry:1:8--1:57:
  • Unsolvable constraint:
      160 == 224
        arising from
        module instantiation
        at Primitive/Asymmetric/Signature/DSA/p1024_sha1.cry:1:8--1:57

We should be able to give a more precise error, of what exactly we were doing when the error occurred (i.e., instantiating a particular parameter, or checking user specified constraints, etc).