Idris String with validation?

Name.idr

-- A data type wrapping a non-empty string
data Name : Type where
  MkName : (s : String) -> (not (s == "") = True) -> Name

-- Some function that expects a valid Name
test : Name -> String
test (MkName s _) = s

-- Usage of that function. Do I need Refl here? Any better way of doing this?
foo : String
foo = test (MkName "foo" Refl)