Typecheck panic

[weaversa]

Cryptol really doesn't like that period after the type assignment. I wonder if it's a parsing issue? This is from the currently nightly.

f : {a} (fin a) => [a] -> (Bit, [a])
f x = (True, x)

g : {a} (fin a) => [a] -> [a]
g x = (f`{a=a} x).1

h = f.1

i : {a} (fin a) => [a] -> [a]
i = f`{a=a}.1

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:  doCheckType
  Message:   TTyApp found when kind checking, but it should have been eliminated already
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:390:24 in cryptol-2.10.0.99-inplace:Cryptol.TypeCheck.Kind
%< ---------------------------------------------------

[brianhuffman]

Here's an example of the same crash using only prelude constants, so you don't need to load a file:

Cryptol> :t splitAt`{3,4,Bool}.0
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  553cbad8b953d501a72d283efd9b8fd18cb5ca38
  Branch:    source-pos (uncommited files present)
  Location:  doCheckType
  Message:   TTyApp found when kind checking, but it should have been eliminated already
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.TypeCheck.Kind
%< ---------------------------------------------------

[brianhuffman]

Using parentheses makes it work, so I'd guess that it probably is a parsing issue.

Cryptol> :t (splitAt`{3,4,Bool}).0
(splitAt`{3, 4, Bool}).0 : [7]Bool -> [3]Bool

[robdockins]

Seems related to #962

[brianhuffman]

I had a closer look at the parser rules, and as I understand it's actually parsing f`{t}.0 as f (`{t}.0), i.e. the field projection .0 binds more tightly than the type application.

[brianhuffman]

I think the problem is in the interaction between the parser and this function mkEApp in the ParserUtils module:

cryptol/src/Cryptol/Parser/ParserUtils.hs

Lines 282 to 310 in 8796390

	-- | Input expression are reversed
	mkEApp :: [Expr PName] -> Expr PName
	mkEApp es@(eLast : _) = at (eFirst,eLast) $ foldl EApp f xs
	where
	eFirst : rest = reverse es
	f : xs = cvtTypeParams eFirst rest
	{- Type applications are parsed as `ETypeVal (TTyApp fs)` expressions.
	Here we associate them with their corresponding functions,
	converting them into `EAppT` constructs. For example:
	[ f, x, `{ a = 2 }, y ]
	becomes
	[ f, x ` { a = 2 }, y ]
	-}
	cvtTypeParams e [] = [e]
	cvtTypeParams e (p : ps) =
	case toTypeParam p of
	Just fs -> cvtTypeParams (EAppT e fs) ps
	Nothing -> e : cvtTypeParams p ps
	toTypeParam e =
	case dropLoc e of
	ETypeVal t -> case dropLoc t of
	TTyApp fs -> Just (map mkTypeInst fs)
	_ -> Nothing
	_ -> Nothing
	mkEApp es = panic "[Parser] mkEApp" ["Unexpected:", show es]

Input expressions of the form f`{t} are parsed as EApp f (ETypeVal (TTyApp t)). Function mkEApp is supposed to then turn this into EAppT f t. When you have input like f`{t}.0, this is parsed as EApp f (ETypeVal (ESel (TTyApp t) (TupleSel 0))). But then that doesn't match the pattern in mkEApp so it gets passed over, even though I think mkEApp is supposed to guarantee that its output doesn't include any TTyApp constructors. That _ -> Nothing case on line 307 looks suspect to me.

[brianhuffman]

Here's an even more direct way to cause a panic:

Cryptol> `{Bool}
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  553cbad8b953d501a72d283efd9b8fd18cb5ca38
  Branch:    source-pos (uncommited files present)
  Location:  doCheckType
  Message:   TTyApp found when kind checking, but it should have been eliminated already
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.TypeCheck.Kind
%< ---------------------------------------------------

Basically, it looks like you can crash cryptol by putting one of these `{t} subexpressions in any place where it is not expected.

[brianhuffman]

Here's another one:

Cryptol> :t join`{4}
join`{4} : {n, a} (fin n) => [4][n]a -> [4 * n]a
Cryptol> :t join(`{4})
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  553cbad8b953d501a72d283efd9b8fd18cb5ca38
  Branch:    source-pos (uncommited files present)
  Location:  doCheckType
  Message:   TTyApp found when kind checking, but it should have been eliminated already
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.10.0.99-5Z4SW1X5RaG67azQhvlix8:Cryptol.TypeCheck.Kind
%< ---------------------------------------------------

[yav]

My guess is that the bug is in translateExprToNumT in Cryptol.Parser.Utils

[brianhuffman]

I don't think translateExprToNumT has anything to do with it. It looks like that only gets called if you use the enumeration syntax.