Insert mutual in "using implementation" blocks
This is important because the totality checker (including the necessary
inlining it needs to do for implementation definitions) runs after every
mutual block, and if it's not there, it doesn't get run when it needs
to, thus missing out the necessary inlining.
Fixes #4194
commitbeb8e9cdb881f540094b4f457fd03d44af116103
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 6 Jan 2018, 12:40 (9 years ago)
parent05634d7
src/Idris/Parser.hs+1
@@ -1796,6 +1796,7 @@ loadSource lidr f toline
17961796 toMutual :: PDecl -> PDecl
17971797 toMutual m@(PMutual _ d) = m
17981798 toMutual (PNamespace x fc ds) = PNamespace x fc (map toMutual ds)
1799+ toMutual (POpenInterfaces f ns ds) = POpenInterfaces f ns (map toMutual ds)
17991800 toMutual x = let r = PMutual (fileFC "single mutual") [x] in
18001801 case x of
18011802 PClauses{} -> r