Fix implicit name bindings in interfaces
This is a special case (which we should try not to make a special case
some day) due to the way implicits are bound in the fields in the record
that results. Now follows the same rules as everything else.
commitc1decaf5bb47853682429c881287143a74d24f71
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 27 Feb 2016, 16:35 (11 years ago)
parent911b97d
libs/contrib/Classes/Verified.idr+1−1
@@ -14,7 +14,7 @@ import Control.Algebra.VectorSpace
1414-- and Monoid).
1515
1616interface Functor f => VerifiedFunctor (f : Type -> Type) where
17− functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
17+ functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x
1818 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
1919 (g1 : a -> b) -> (g2 : b -> c) ->
2020 map (g2 . g1) x = (map g2 . map g1) x
src/Idris/AbsSyntax.hs+1−1
@@ -1593,7 +1593,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
15931593 -- binding
15941594 -- Not the function position, but do everything else...
15951595 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1596− implNamesIn uv t = namesIn uv ist t
1596+ implNamesIn uv t = implicitNamesIn (map fst uv) ist t
15971597
15981598 imps top env ty@(PApp _ f as)
15991599 = do (decls, ns) <- get