Newtype/enum expression causes core lint to panic

[RyanGlScott]

// Bar.cry
newtype T = { unT : [8] }

f : T
f = T { unT = 0 }

// Bar.icry
:set coreLint=true
:l Bar.cry

$ ~/Software/cryptol-3.0.0/bin/cryptol -b Bar.icry 
Loading module Cryptol
Loading module Cryptol
{n, a, b, c} n == min n n
{a, n} (fin n) => inf == inf * (1 * (1 * 1))
{a, n} (fin n) => n / 2 == n - n /^ 2
{n, a, b} n == min n n
{n} (n >= 1, fin n) => (fin n, n >= 1)
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:  7aede559ad102b0ccdaf4b377d3fa17cc564286e
  Branch:    release-3.0.0 (uncommited files present)
  Location:  Core lint failed:
  Message:   Location: Bar.cry:5:5--5:6
             Undefined variable
  • Variable: Main::T
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/Base.hs:717:29 in cryptol-3.0.0-inplace:Cryptol.ModuleSystem.Base
%< ---------------------------------------------------

A similar issue exists for enum constructors on the sum-types (#1602) as well:

// Foo.cry
enum T = MkT

f : T
f = MkT

// Foo.icry
:set coreLint=true
:l Foo.cry

$ cabal run exe:cryptol -- -b Foo.icry 
Loading module Cryptol
Loading module Cryptol
{n, a, b, c} n == min n n
{a, n} (fin n) => inf == inf * (1 * (1 * 1))
{a, n} (fin n) => n / 2 == n - n /^ 2
{n, a, b} n == min n n
{n} (n >= 1, fin n) => (fin n, n >= 1)
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:  a6b48b41d54798ea376d26255ad315178752ab93
  Branch:    sum-types (uncommited files present)
  Location:  Core lint failed:
  Message:   Location: Foo.cry:5:5--5:8
             Undefined variable
  • Variable: Main::MkT
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/Base.hs:732:29 in cryptol-3.0.0.99-inplace:Cryptol.ModuleSystem.Base
%< ---------------------------------------------------

[yav]

That's likely because we need to fill in the missing bit in Sanity

[RyanGlScott]

Which missing bit are you referring to? I think this issue is separate from #1615 since it affects newtypes, not just enums.

[yav]

You are correct---the issue that we are not adding the types of constructors to the environment. I am in the process of fixing it.