Inline type declaration

[weaversa]

Is it possible to define a type variable (or a relationship between types) without explicitly creating a new variable?

For example:

fibs = basecase # (drop`{BaseCaseSize} fibs')
  where
    type BaseCaseSize = 2
    basecase = [0, 1] : [BaseCaseSize]_
    fibs'@i = fibs@(i-1) + fibs@(i-2)

It would be nice to be able to use the size of the basecase in the drop statement, without having to give the size. Something like this?

fibs = basecase # (drop`{BaseCaseSize} fibs')
  where
    basecase = [0, 1] : [BaseCaseSize]_
    fibs'@i = fibs@(i-1) + fibs@(i-2)

Cryptol used to accept something like:

fibs = basecase # (drop`{width basecase} fibs')
  where
    basecase = [0, 1]
    fibs'@i = fibs@(i-1) + fibs@(i-2)

I just don't know how to give this type a name without specifying the concrete value 2.

[weaversa]

Here's another possibility that looks more like the explicit type annotations for functions (f (x : t) = ...) from the syntax manual.

fibs = basecase # (drop`{BaseCaseSize} recurrence)
  where
    (basecase : [BaseCaseSize]_) = [0, 1]
    recurrence@i = fibs@(i-1) + fibs@(i-2)

[atomb]

This seems somewhat related to #814, but at the type level instead of the value level.