Sum types

[yav]

This branch implements non-recursive nominal sum types for Cryptol. See also #1588.

[RyanGlScott]

With my most recent push, I believe all of the remaining work has been completed. The one thing that is missing is deriving support (#1587), but we can defer this for later.

@yav, do you have any review comments? The things that are new since the last time you looked are:

1. A mention of this work in CHANGES.md
2. Adding Option and Result to the Cryptol standard library
3. Documentation thereof in the reference manual

We should also try updating GaloisInc/saw-script#2020 once more.

[RyanGlScott]

The failing CI on GaloisInc/saw-script#2020 in this job reveals a regression in the way Cryptol handles abstract types. Cryptol 3.0.0 accepts this:

module Either where

primitive type Either : * -> * -> *
primitive Left : {a, b} a -> Either a b

But it now rejects it with the sum-types branch:

$ cabal run exe:cryptol -- Either.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0.99 (a6b48b4, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Either
[error] at Either.cry:4:30--4:40:
  Malformed type.
    Type synonym `Either::Either` was applied to 2 extra parameterss.

(There's also a typo in "parameterss".)

I'll mark this PR as a draft until we sort this out.

[RyanGlScott]

Ah, I think the problem lies in this code:

cryptol/src/Cryptol/TypeCheck/Kind.hs

Lines 339 to 361 in a9e35fe

	checkNominalTypeUse nt
	| Abstract <- ntDef nt, Just tc <- builtInType (ntName nt) =
	do (ts1,k1) <- appTy ts (kindOf tc)
	let as = ntParams nt
	ps = ntConstraints nt
	case as of
	[] -> pure ()
	_ -> do let need = length as
	have = length ts1
	when (need > have) $
	kRecordError (TooFewTyParams (ntName nt) (need - have))
	let su = listSubst (map tpVar as `zip` ts1)
	kNewGoals (CtPartialTypeFun (ntName nt)) (apSubst su <$> ps)
	checkKind (TCon tc ts1) k k1
	| otherwise =
	do (ts1,k1) <- appTy ts (kindOf nt)
	let as = ntParams nt
	ts2 <- checkParams as ts1
	let su = zip as ts2
	ps1 <- mapM (`kInstantiateT` su) (ntConstraints nt)
	kNewGoals (CtPartialTypeFun (ntName nt)) ps1
	checkKind (TNominal nt ts2) k k1

The case that handles Abstract types only fires if builtInType returns Just. In the example above, however, Example is not a built-in type, so builtInType returns Nothing. Therefore, it falls through to the case that is supposed to handle newtypes and enums, which leads to disaster.

Relatedly, we ought to change the error messages for TooFewTyParams and TooManyTySynParams to say something besides "Type synonym" when the error involves a nominal type.

[RyanGlScott]

I've pushed a fix for the issue described in #1602 (comment) in commit ca0eb7e.