Matching on different types error

sigma_break.idr

%default total
data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

F : MyList a -> Maybe Type
F [] = Nothing
F ((::) {a} x xs) = Just a

G : MyList a -> Maybe Type
G [] {a} = Just a
G (x :: xs) = Nothing

data Check : Maybe Type -> Type where
  Right : (me : MyList a) -> Check (F me)
  Fight : (me : MyList a) -> Check (G me)

switch : Check a -> (b : Maybe Type ** Check b)
switch (Right me) = (_ ** Fight me)
switch (Fight me) = (_ ** Right me)

switch2 : (a : Maybe Type ** Check a) -> (b : Maybe Type ** Check b)
switch2 (_ ** Right me) = ?test1
switch2 (_ ** Fight me) = ?test2