@@ -48,17 +48,21 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
4848 let ty = addImpl i ty'
4949 logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'
5050 logLvl 2 $ show n ++ " type " ++ showImp True ty
51− ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []
51+ ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []
5252 (erun fc (build i info False n ty))
53− (cty, _) <- recheckC ctxt fc [] ty'
53+ ds <- checkDef fc defer
54+ addDeferred ds
55+ mapM_ (elabCaseBlock info) is
56+ ctxt <- getContext
57+ (cty, _) <- recheckC ctxt fc [] tyT
58+ addStatics n cty ty'
5459 logLvl 2 $ "---> " ++ show cty
5560 let nty = normalise ctxt [] cty
56− ds <- checkDef fc ((n, nty):defer)
61+ ds <- checkDef fc [(n, nty)]
5762 addIBC (IBCDef n)
5863 addDeferred ds
5964 setFlags n opts
6065 addIBC (IBCFlags n opts)
61− mapM_ (elabCaseBlock info) is
6266
6367elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
6468elabData info syn fc (PDatadecl n t_in dcons)