Higher-kinded/Prop type variables?

[robdockins]

Currently, you are allowed to write down the following type alias and have it accepted by the type checker.

type Funny (f : # -> *) = Integer

This is pretty strange, as I don't think you can actually do anything interesting with higher-kinded type variables. The following two lines each generate an error, for example.

type Funny2 (f:# -> *) = f 100
type Asdf = Funny Z

You can also write this, which is pretty odd:

type Strange (f : Prop) = Integer

Again, there isn't really anything interesting you can do with this type, as you cannot assert the Prop anywhere.

I think that for type and newtype declarations, we should probably restrict the kinds of parameters to either * or #.

[robdockins]

Oh, this is fun too.

funnyFunc : { f : # -> * } Integer
funnyFunc = zero

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

%< ---------------------------------------------------
  Revision:  66cdf6755321ed1169bbfafbb0a95bfb9f4eeaa2
  Branch:    reals (uncommited files present)
  Location:  [Eval] evalExpr
  Message:   invalid kind on type abstraction
             KNum :-> KType
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/Eval.hs:186:16 in cryptol-2.10.0.99-inplace:Cryptol.Eval
%< ---------------------------------------------------

[brianhuffman]

I think we should split the Kind datatype into two: one datatype for "base" kinds, and another datatype for function kinds.

data Kind = KProp | KNum | KType
data KFun = KFun [Kind] Kind

This would be a more precise fit for the Cryptol language: Then type variables have a Kind, and type constructors have a KFun. We wouldn't even be able to express the weird definitions in the original post.

[yav]

I think I know what happened here---it used to be the case the you couldn't even write these in the parser, so we probably didn't do much checking. Then when I added abstract type declarations (e.g., the primitive type in the Prelude), I modified the parser to allow writing function kinds, but probably forgot to check that they don't show up in other places.

I think it should be relatively easy to check for this in the kind checker. I am not sure it is worth splitting the Kind type... Who knows, maybe one day we'd want to add higher kinded type variables :)

[robdockins]

I don't have a strong opinion on splitting the kind datatype. Either way, I think we'll need to check that Prop doesn't appear in places other than module parameters.

[robdockins]

Should we allow declarations like this? It's currently allowed and seems sensible, although it doesn't really work great as you can only put a single atomic constraint in the actual argument position.

type constraint PredSyn (a : *) (p:Prop) = (Zero a, Cmp a, p)

someFunc : {a} (PredSyn a (Logic a)) => a
someFunc = ~zero