「checkSimple」は、ユニバースUの要素であるuを取得し、（nat 1）がuで指定されたagdaタイプに変換できるかどうかをチェックします。変換の結果が返されます。
次に、コンソールプログラムを作成して、コマンドラインから「someU」を取得しようとしています。
そのため、「checkSimple」のタイプを変更して、パラメーターとして（u：たぶんU）を含めました（たぶん、コンソールからの入力は「nothing」である可能性があるため）。ただし、タイプチェックするコードを取得できません。
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)
-}