(TypeT src vs, [TypeT src vs])
spineTy typ = go [] typ
where
- go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
+ go :: forall kx (x::kx). [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
| Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
= go ctx t -- NOTE: skip the constraint @q@.