@@ -49,8 +49,13 @@ checkDef fc ns = do ctxt <- getContext
49-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
49-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
50elabType :: ElabInfo -> SyntaxInfo -> String ->
50elabType :: ElabInfo -> SyntaxInfo -> String ->
51 FC -> FnOpts -> Name -> PTerm -> Idris Type
51 FC -> FnOpts -> Name -> PTerm -> Idris Type
52+elabType = elabType' False
54+elabType' :: Bool -> -- normalise it
55+ ElabInfo -> SyntaxInfo -> String ->
56+ FC -> FnOpts -> Name -> PTerm -> Idris Type
52−elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
57+elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
53− n = liftname info n_in in -}
58+ n = liftname info n_in in -}
54 do checkUndefined fc n
59 do checkUndefined fc n
55 ctxt <- getContext
60 ctxt <- getContext
56 i <- getIState
61 i <- getIState
@@ -90,7 +95,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
90 _ -> False
95 _ -> False
91 _ -> False
96 _ -> False
92 let opts' = if corec then (Coinductive : opts) else opts
97 let opts' = if corec then (Coinductive : opts) else opts
98+ let usety = if norm then nty' else nty
93− ds <- checkDef fc [(n, (-1, Nothing, nty))]
99+ ds <- checkDef fc [(n, (-1, Nothing, usety))]
94 addIBC (IBCDef n)
100 addIBC (IBCDef n)
95 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
101 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
96 addDeferred ds'
102 addDeferred ds'
@@ -102,7 +108,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
102 addIBC (IBCCoercion n)
108 addIBC (IBCCoercion n)
103 when corec $ do setAccessibility n Frozen
109 when corec $ do setAccessibility n Frozen
104 addIBC (IBCAccess n Frozen)
110 addIBC (IBCAccess n Frozen)
105− return nty
111+ return usety
107 -- for making an internalapp, we only want the explicit ones, and don't
113 -- for making an internalapp, we only want the explicit ones, and don't
108 -- want the parameters, so just take the arguments which correspond to the
114 -- want the parameters, so just take the arguments which correspond to the
@@ -1411,14 +1417,14 @@ elabInstance info syn fc cs n ps t expn ds
1411 Nothing -> SN (InstanceN n (map show ps))
1417 Nothing -> SN (InstanceN n (map show ps))
1412 -- UN ('@':show n ++ "$" ++ show ps)
1418 -- UN ('@':show n ++ "$" ++ show ps)
1413 Just nm -> nm
1419 Just nm -> nm
1420+ nty <- elabType' True info syn "" fc [] iname t
1414 -- if the instance type matches any of the instances we have already,
1421 -- if the instance type matches any of the instances we have already,
1415 -- and it's not a named instance, then it's overlapping, so report an error
1422 -- and it's not a named instance, then it's overlapping, so report an error
1416 case expn of
1423 case expn of
1417− Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
1424+ Nothing -> do mapM_ (checkNotOverlapping i (delab i nty))
1425+ (class_instances ci)
1418 addInstance intInst n iname
1426 addInstance intInst n iname
1419 Just _ -> addInstance intInst n iname
1427 Just _ -> addInstance intInst n iname
1420− tt_ty <- elabType info syn "" fc [] iname t
1421− let nty = normalise (tt_ctxt i) [] tt_ty
1422 let ips = zip (class_params ci) ps
1428 let ips = zip (class_params ci) ps
1423 let ns = case n of
1429 let ns = case n of
1424 NS n ns' -> ns'
1430 NS n ns' -> ns'