type error: no instance of 'Component on ???
in testdata/adhoc.reject.lc:4:5:
x = one :: Vec 4 A
    ^^^

------------ trace
'A :: Type
A :: 'A
'ACase :: (a : 'A->Type) -> a A -> b:'A -> a b
match'A :: (a : Type->Type) -> a 'A -> b:Type -> a b -> a b
!type error: no instance of 'Component on ???
in testdata/adhoc.reject.lc:4:5:
x = one :: Vec 4 A
    ^^^

------------ tooltips
testdata/adhoc.reject.lc 2:6-2:7  Type
testdata/adhoc.reject.lc 2:6-2:11  Type
testdata/adhoc.reject.lc 2:10-2:11  A
testdata/adhoc.reject.lc 4:5-4:8  {a} -> {_ : Component a}->a
testdata/adhoc.reject.lc 4:12-4:15  Nat -> Type->Type
testdata/adhoc.reject.lc 4:12-4:17  Type->Type
testdata/adhoc.reject.lc 4:12-4:19  Type
testdata/adhoc.reject.lc 4:16-4:17  b_
testdata/adhoc.reject.lc 4:18-4:19  Type