git.iko.soy/Idris-dev
on master help sign in
Fixes for GHC 8.6
77bae41Niklas Larsson
src/Idris/Core/CaseTree.hs+4−4
compare with master
unifiedsplit
@@ -549,19 +549,19 @@ caseGroups (v:vs) gs err = do g <- altGroups gs
549
549
550 altGroup n i args
550 altGroup n i args
551 = do inacc <- inaccessibleArgs n
551 = do inacc <- inaccessibleArgs n
552− (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
552+ ~(newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
553 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
553 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
554 return $ ConCase n i newVars matchCs
554 return $ ConCase n i newVars matchCs
555
555
556− altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
556+ altFnGroup n args = do ~(newVars, _, [], nextCs) <- argsToAlt [] args
557 matchCs <- match (newVars ++ vs) nextCs err
557 matchCs <- match (newVars ++ vs) nextCs err
558 return $ FnCase n newVars matchCs
558 return $ FnCase n newVars matchCs
559
559
560− altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
560+ altSucGroup args = do ~([newVar], _, [], nextCs) <- argsToAlt [] args
561 matchCs <- match (newVar:vs) nextCs err
561 matchCs <- match (newVar:vs) nextCs err
562 return $ SucCase newVar matchCs
562 return $ SucCase newVar matchCs
563
563
564− altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
564+ altConstGroup n args = do ~(_, _, [], nextCs) <- argsToAlt [] args
565 matchCs <- match vs nextCs err
565 matchCs <- match vs nextCs err
566 return $ ConstCase n matchCs
566 return $ ConstCase n matchCs
567
567
src/Idris/Elab/Term.hs+4−4
@@ -448,7 +448,7 @@ elab ist info emode opts fn tm
448 -- the full set.
448 -- the full set.
449 uns <- get_usedns
449 uns <- get_usedns
450 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
450 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
451− (h : hs) <- get_holes
451+ ~(h : hs) <- get_holes
452 ty <- goal
452 ty <- goal
453 case as' of
453 case as' of
454 [] -> do hds <- mapM showHd as
454 [] -> do hds <- mapM showHd as
@@ -984,7 +984,7 @@ elab ist info emode opts fn tm
984 (elab' ina fc Placeholder)
984 (elab' ina fc Placeholder)
985 (show f)
985 (show f)
986 elab' ina fc Placeholder
986 elab' ina fc Placeholder
987− = do (h : hs) <- get_holes
987+ = do ~(h : hs) <- get_holes
988 movelast h
988 movelast h
989 elab' ina fc (PMetavar nfc n) =
989 elab' ina fc (PMetavar nfc n) =
990 do ptm <- get_term
990 do ptm <- get_term
@@ -1251,7 +1251,7 @@ elab ist info emode opts fn tm
1251 elab' ina fc (PHidden t)
1251 elab' ina fc (PHidden t)
1252 | reflection = elab' ina fc t
1252 | reflection = elab' ina fc t
1253 | otherwise
1253 | otherwise
1254− = do (h : hs) <- get_holes
1254+ = do ~(h : hs) <- get_holes
1255 -- Dotting a hole means that either the hole or any outer
1255 -- Dotting a hole means that either the hole or any outer
1256 -- hole (a hole outside any occurrence of it)
1256 -- hole (a hole outside any occurrence of it)
1257 -- must be solvable by unification as well as being filled
1257 -- must be solvable by unification as well as being filled
@@ -1259,7 +1259,7 @@ elab ist info emode opts fn tm
1259 -- Delay dotted things to the end, then when we elaborate them
1259 -- Delay dotted things to the end, then when we elaborate them
1260 -- we can check the result against what was inferred
1260 -- we can check the result against what was inferred
1261 movelast h
1261 movelast h
1262− (h' : hs) <- get_holes
1262+ ~(h' : hs) <- get_holes
1263 -- If we're at the end anyway, do it now
1263 -- If we're at the end anyway, do it now
1264 if h == h' then elabHidden h
1264 if h == h' then elabHidden h
1265 else delayElab 10 $ elabHidden h
1265 else delayElab 10 $ elabHidden h
src/Idris/Parser/Stack.hs+2−2
@@ -117,9 +117,9 @@ addExtent = tell
117-- extent is taking trailing whitespace, it's likely there's a double-wrapped
117-- extent is taking trailing whitespace, it's likely there's a double-wrapped
118-- parser (usually via @Idris.Parser.Helpers.token@).
118-- parser (usually via @Idris.Parser.Helpers.token@).
119trackExtent :: Parsing m => m a -> m a
119trackExtent :: Parsing m => m a -> m a
120−trackExtent p = do (FC f (sr, sc) _) <- getFC
120+trackExtent p = do ~(FC f (sr, sc) _) <- getFC
121 result <- p
121 result <- p
122− (FC f _ (er, ec)) <- getFC
122+ ~(FC f _ (er, ec)) <- getFC
123 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
123 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
124 return result
124 return result
125
125