can the following Lean type be expressed in haskell? inductive mytype | mk : a -> mytype