Agda: my code does not print a check (how to get implicit arguments correctly?)

"checkSimple" gets u, the universe element is U and checks (nat 1) can be converted to the agda type given by u. The result of the conversion is returned.

Now I am trying to write a console program and get "someU" from the command line.

So I changed the type of "checkSimple" to include the parameter (u: Maybe U) as the parameter (perhaps because the console input might be "nothing"). However, I can not get the code to check the type.

module CheckMain where


open import Prelude

-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude

-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory 



data S : Set where
  nat  : (n : ℕ) → S
  nil  : S

sToℕ : S → Maybe ℕ
sToℕ (nat n) = just n
sToℕ _       = nothing


data U : Set where
  nat     : U

El : U → Set
El nat = ℕ


sToStat : (u : U) → S → Maybe (El u)
sToStat nat           s = sToℕ s


-- Basic Test
test1 : Maybe ℕ
test1 = sToStat nat (nat 1)


{- THIS WORKS -}

checkSimple : (u : U) → Maybe (El u)
checkSimple someU = sToStat someU (nat 1)



{- HERE IS THE ERROR -}

-- in contrast to checkSimple we only get a (Maybe U) as a parameter
-- (e.g. from console input)

check : {u : U} (u1 : Maybe U) → Maybe (El u)
check (just someU) = sToStat someU (nat 1)
check _ = nothing


{- HER IS THE ERROR MESSAGE -}

{- 
someU != .u of type U
when checking that the expression sToStat someU (nat 1) has type
Maybe (El .u)
-}