A rule with nested constructors does not typecheck when it should.

[FranchuFranchu]

The following code does not typecheck in kind2 0.2.79, and the current master branch neither.

Wrapper <a>: Type
Wrapper.new <a> (v: a): Wrapper a
MyFn (w: Wrapper (Wrapper U60)): U60
MyFn (Wrapper.new (Wrapper.new a)) = a

It fails with

Type mismatch
- Expected: U60
- Detected: a0_
Kind.Context:
- a1_ : Type
- a1_ = (Wrapper U60)
- a1_ = (Wrapper a0_)
- a0_ : Type
- a   : a0_
On 'test.kind2':
   5 | MyFn (Wrapper.new (Wrapper.new a)) = a

[atennapel]

Just a guess: what if you do Wrapper (a : Type) : Type? I'm just looking at how List is defined in https://github.com/Kindelia/Kind/blob/master/example/example.kind2 .

[developedby]

Kind doesn't do this type of unification, you need to manually indicate to the type checker that these things are the same (by clever use of lets and annotations, type rewrites or the subst syntax), although I can never remember the right way to do it.

You could also break the nested pattern into two functions like this

Wrapper (a: Type) : Type
Wrapper.new <a> (v: a): Wrapper a

DoubleUnwrap <t: Type> (w: Wrapper (Wrapper t)) : t
DoubleUnwrap (Wrapper.new a) = Unwrap a

Unwrap <t: Type> (w: Wrapper t) : t
Unwrap (Wrapper.new a) = a

What @atennapel is not relevant in this case, but you probably don't want to declare your type with implicit parameter a since it could lead to unexpected type inferences