8c2a516 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Overidable overlapping implementation check

Using %overlapping flag on the implementation In theory, this should never be necessary, but in practice there are situations where Idris might think implementations are overlapping, e.g. of the form "Foo a => Bar a", where there are other implementations of Bar without the superclass constraint. So, the check needs to be better, but it's a fairly big task so this is a workaround for the moment.

commit8c2a516c3952e2e730a80f1038e9405010b1df1b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 2 Oct 2016, 14:47 (10 years ago) parent97319d9

4 files changed+11−2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Elab/Implementation.hs+6−2 src/Idris/IBC.hs+2 src/Idris/Parser.hs+2

src/Idris/AbsSyntaxTree.hs+1

@@ -641,6 +641,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

641641 -- | interface dictionary, eval only when a function

642642 -- argument, and further evaluation results.

643643 | Dictionary

644+ | OverlappingDictionary -- ^ Interface dictionary which may overlap

644645 | Implicit -- ^ implicit coercion

645646 | NoImplicit -- ^ do not apply implicit coercions

646647 | CExport String -- ^ export, with a C name

src/Idris/Elab/Implementation.hs+6−2

@@ -93,10 +93,12 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

9393 -- if the implementation type matches any of the implementations we have already,

9494 -- and it's not a named implementation, then it's overlapping, so report an error

9595 case expn of

96− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

96+ Nothing

97+ | OverlappingDictionary `notElem` opts ->

98+ do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

9799 (map fst $ interface_implementations ci)

98100 addImplementation intImpl True n iname

99− Just _ -> addImplementation intImpl False n iname

101+ _ -> addImplementation intImpl False n iname

100102 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do

101103 -- Add the parent implementation names to the privileged set

102104 oldOpen <- addOpenImpl parents

@@ -255,6 +257,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

255257

256258 findOverlapping i dets t n

257259 | SN (ParentN _ _) <- n = Nothing

260+ | Just opts <- lookupCtxtExact n (idris_flags i),

261+ OverlappingDictionary `elem` opts = Nothing

258262 | otherwise

259263 = case lookupTy n (tt_ctxt i) of

260264 [t'] -> let tret = getRetType t

src/Idris/IBC.hs+2

@@ -1222,6 +1222,7 @@ instance Binary FnOpt where

12221222 AutoHint -> putWord8 15

12231223 PEGenerated -> putWord8 16

12241224 StaticFn -> putWord8 17

1225+ OverlappingDictionary -> putWord8 18

12251226 get

12261227 = do i <- getWord8

12271228 case i of

@@ -1245,6 +1246,7 @@ instance Binary FnOpt where

12451246 15 -> return AutoHint

12461247 16 -> return PEGenerated

12471248 17 -> return StaticFn

1249+ 18 -> return OverlappingDictionary

12481250 _ -> error "Corrupted binary data for FnOpt"

12491251

12501252instance Binary Fixity where

src/Idris/Parser.hs+2

@@ -691,6 +691,8 @@ fnOpt = do reservedHL "total"; return TotalFn

691691 return Reflection

692692 <|> do try (lchar '%' *> reserved "hint");

693693 return AutoHint

694+ <|> do try (lchar '%' *> reserved "overlapping");

695+ return OverlappingDictionary

694696 <|> do lchar '%'; reserved "specialise";

695697 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

696698 return $ Specialise ns