basic018.idr:7:12-16:
  |
7 |       Vect thing elem
  |            ~~~~~
thing is bound as an implicit
	Did you mean to refer to Main.thing?

basic018.idr:12:8-12:
   |
12 | test : thing = S 41
   |        ~~~~~
thing is bound as an implicit
	Did you mean to refer to Main.thing?

basic018.idr:13:8-11:
   |
13 | test = Refl
   |        ~~~~
When checking right hand side of test with expected type
        thing = S 41

Type mismatch between
        42 = 42 (Type of Refl)
and
        thing = 42 (Expected type)

Specifically:
        Type mismatch between
                42
        and
                thing