git.iko.soy/Idris-dev
on master help sign in
Fix implicit name bindings in interfaces
c1decafEdwin Brady
libs/contrib/Classes/Verified.idr+1−1
compare with master
unifiedsplit
@@ -14,7 +14,7 @@ import Control.Algebra.VectorSpace
14-- and Monoid).
14-- and Monoid).
15
15
16interface Functor f => VerifiedFunctor (f : Type -> Type) where
16interface 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
18 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
18 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
19 (g1 : a -> b) -> (g2 : b -> c) ->
19 (g1 : a -> b) -> (g2 : b -> c) ->
20 map (g2 . g1) x = (map g2 . map g1) x
20 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) $
1593 -- binding
1593 -- binding
1594 -- Not the function position, but do everything else...
1594 -- Not the function position, but do everything else...
1595 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1595 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
1597
1597
1598 imps top env ty@(PApp _ f as)
1598 imps top env ty@(PApp _ f as)
1599 = do (decls, ns) <- get
1599 = do (decls, ns) <- get