@@ -284,6 +284,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
284284 checkDocs fc argDocs t_in
285285 addDocStr n doc argDocs
286286 addIBC (IBCDoc n)
287+ addIBC (IBCOpt n)
287288 let metainf = DataMI params
288289 addIBC (IBCMetaInformation n metainf)
289290 -- TMP HACK! Make this a data option
@@ -291,11 +292,24 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
291292 updateContext (addDatatype (Data n ttag cty cons))
292293 updateContext (setMetaInformation n metainf)
293294 mapM_ (checkPositive n) cons
295+
296+ case cons of
297+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n
298+ _ -> return ()
299+
294300 if DefaultEliminator `elem` opts
295301 then evalStateT (elabEliminator params n t dcons info) Map.empty
296302 else return ()
297303 where
298− checkDefinedAs fc n t ctxt
304+ setDetaggable :: Name -> Idris ()
305+ setDetaggable n = do
306+ ist <- getIState
307+ let opt = idris_optimisation ist
308+ case lookupCtxt n opt of
309+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
310+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise False False [] [] [] True) opt }
311+
312+ checkDefinedAs fc n t ctxt
299313 = case lookupDef n ctxt of
300314 [] -> return ()
301315 [TyDecl _ ty] ->