git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4562 from melted/support_ghc86

Fixes for GHC 8.6

commit60c5b3eadbffdbad08b975fc2b7b0649725ce342 authorNiklas Larsson <metaniklas@gmail.com> dateSun 16 Sep 2018, 17:26 (8 years ago) parent4d8dab077bae41
3 files changed+10−10
compare with master
unifiedsplit
src/Idris/Core/CaseTree.hs+4−4 src/Idris/Elab/Term.hs+4−4 src/Idris/Parser/Stack.hs+2−2
src/Idris/Core/CaseTree.hs+4−4
@@ -549,19 +549,19 @@ caseGroups (v:vs) gs err = do g <- altGroups gs
549549
550550 altGroup n i args
551551 = do inacc <- inaccessibleArgs n
552− (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
552+ ~(newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
553553 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
554554 return $ ConCase n i newVars matchCs
555555
556− altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
556+ altFnGroup n args = do ~(newVars, _, [], nextCs) <- argsToAlt [] args
557557 matchCs <- match (newVars ++ vs) nextCs err
558558 return $ FnCase n newVars matchCs
559559
560− altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
560+ altSucGroup args = do ~([newVar], _, [], nextCs) <- argsToAlt [] args
561561 matchCs <- match (newVar:vs) nextCs err
562562 return $ SucCase newVar matchCs
563563
564− altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
564+ altConstGroup n args = do ~(_, _, [], nextCs) <- argsToAlt [] args
565565 matchCs <- match vs nextCs err
566566 return $ ConstCase n matchCs
567567
src/Idris/Elab/Term.hs+4−4
@@ -448,7 +448,7 @@ elab ist info emode opts fn tm
448448 -- the full set.
449449 uns <- get_usedns
450450 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
451− (h : hs) <- get_holes
451+ ~(h : hs) <- get_holes
452452 ty <- goal
453453 case as' of
454454 [] -> do hds <- mapM showHd as
@@ -984,7 +984,7 @@ elab ist info emode opts fn tm
984984 (elab' ina fc Placeholder)
985985 (show f)
986986 elab' ina fc Placeholder
987− = do (h : hs) <- get_holes
987+ = do ~(h : hs) <- get_holes
988988 movelast h
989989 elab' ina fc (PMetavar nfc n) =
990990 do ptm <- get_term
@@ -1251,7 +1251,7 @@ elab ist info emode opts fn tm
12511251 elab' ina fc (PHidden t)
12521252 | reflection = elab' ina fc t
12531253 | otherwise
1254− = do (h : hs) <- get_holes
1254+ = do ~(h : hs) <- get_holes
12551255 -- Dotting a hole means that either the hole or any outer
12561256 -- hole (a hole outside any occurrence of it)
12571257 -- must be solvable by unification as well as being filled
@@ -1259,7 +1259,7 @@ elab ist info emode opts fn tm
12591259 -- Delay dotted things to the end, then when we elaborate them
12601260 -- we can check the result against what was inferred
12611261 movelast h
1262− (h' : hs) <- get_holes
1262+ ~(h' : hs) <- get_holes
12631263 -- If we're at the end anyway, do it now
12641264 if h == h' then elabHidden h
12651265 else delayElab 10 $ elabHidden h
src/Idris/Parser/Stack.hs+2−2
@@ -117,9 +117,9 @@ addExtent = tell
117117-- extent is taking trailing whitespace, it's likely there's a double-wrapped
118118-- parser (usually via @Idris.Parser.Helpers.token@).
119119trackExtent :: Parsing m => m a -> m a
120−trackExtent p = do (FC f (sr, sc) _) <- getFC
120+trackExtent p = do ~(FC f (sr, sc) _) <- getFC
121121 result <- p
122− (FC f _ (er, ec)) <- getFC
122+ ~(FC f _ (er, ec)) <- getFC
123123 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
124124 return result
125125