@@ -49,8 +49,13 @@ checkDef fc ns = do ctxt <- getContext
4949-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
5050elabType :: ElabInfo -> SyntaxInfo -> String ->
5151 FC -> FnOpts -> Name -> PTerm -> Idris Type
52−elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
53− n = liftname info n_in in -}
52+elabType = elabType' False
53+
54+elabType' :: Bool -> -- normalise it
55+ ElabInfo -> SyntaxInfo -> String ->
56+ FC -> FnOpts -> Name -> PTerm -> Idris Type
57+elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
58+ n = liftname info n_in in -}
5459 do checkUndefined fc n
5560 ctxt <- getContext
5661 i <- getIState
@@ -90,7 +95,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
9095 _ -> False
9196 _ -> False
9297 let opts' = if corec then (Coinductive : opts) else opts
93− ds <- checkDef fc [(n, (-1, Nothing, nty))]
98+ let usety = if norm then nty' else nty
99+ ds <- checkDef fc [(n, (-1, Nothing, usety))]
94100 addIBC (IBCDef n)
95101 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
96102 addDeferred ds'
@@ -102,7 +108,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
102108 addIBC (IBCCoercion n)
103109 when corec $ do setAccessibility n Frozen
104110 addIBC (IBCAccess n Frozen)
105− return nty
111+ return usety
106112 where
107113 -- for making an internalapp, we only want the explicit ones, and don't
108114 -- 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
14111417 Nothing -> SN (InstanceN n (map show ps))
14121418 -- UN ('@':show n ++ "$" ++ show ps)
14131419 Just nm -> nm
1420+ nty <- elabType' True info syn "" fc [] iname t
14141421 -- if the instance type matches any of the instances we have already,
14151422 -- and it's not a named instance, then it's overlapping, so report an error
14161423 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)
14181426 addInstance intInst n iname
14191427 Just _ -> addInstance intInst n iname
1420− tt_ty <- elabType info syn "" fc [] iname t
1421− let nty = normalise (tt_ctxt i) [] tt_ty
14221428 let ips = zip (class_params ci) ps
14231429 let ns = case n of
14241430 NS n ns' -> ns'