@@ -90,7 +90,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9090 Nothing -> transformPats ist pats_in
9191 _ -> pats_in
9292
93− let pats = map (simple_lhs (tt_ctxt ist)) $
93+ let pats = map (simple_lhs (tt_ctxt ist)) $
9494 doPartialEval ist tpats
9595
9696 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
@@ -257,7 +257,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
257257
258258 getLHS (_, l, _) = l
259259
260− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
260+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
261261 force (normalisePats ctxt [] y))
262262 simple_lhs ctxt t = t
263263
@@ -265,10 +265,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
265265 (rt_simplify ctxt [] y)))
266266
267267 -- this is so pattern types are in the right form for erasure
268− normalisePats ctxt env (Bind n (PVar t) sc)
268+ normalisePats ctxt env (Bind n (PVar t) sc)
269269 = let t' = normalise ctxt env t in
270270 Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)
271− normalisePats ctxt env (Bind n (PVTy t) sc)
271+ normalisePats ctxt env (Bind n (PVTy t) sc)
272272 = let t' = normalise ctxt env t in
273273 Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)
274274 normalisePats ctxt env t = t
@@ -284,7 +284,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
284284 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
285285 sameLength [] = return 0
286286
287− -- Partially evaluate, if the definition is marked as specialisable
287+ -- Partially evaluate, if the definition is marked as specialisable
288288 doPartialEval ist pats =
289289 case specNames opts of
290290 Nothing -> pats
@@ -296,14 +296,14 @@ elabPE info fc caller r =
296296 do ist <- getIState
297297 let sa = getSpecApps ist [] r
298298 mapM_ (mkSpecialised ist) sa
299− where
300− -- Make a specialised version of the application, and
301− -- add a PTerm level transformation rule, which is basically the
302− -- new definition in reverse (before specialising it).
303− -- RHS => LHS where implicit arguments are left blank in the
299+ where
300+ -- Make a specialised version of the application, and
301+ -- add a PTerm level transformation rule, which is basically the
302+ -- new definition in reverse (before specialising it).
303+ -- RHS => LHS where implicit arguments are left blank in the
304304 -- transformation.
305305
306− -- Transformation rules are applied after every PClause elaboration
306+ -- Transformation rules are applied after every PClause elaboration
307307
308308 mkSpecialised ist specapp_in = do
309309 let (specTy, specapp) = getSpecTy ist specapp_in
@@ -315,7 +315,7 @@ elabPE info fc caller r =
315315 idrisCatch
316316 (when (undef && all (concreteArg ist) (snd specapp)) $ do
317317 cgns <- getAllNames n
318− let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++
318+ let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++
319319 mapMaybe specName (snd specapp))]
320320 logLvl 3 $ "Specialising application: " ++ show specapp
321321 ++ " with " ++ show cgns
@@ -323,25 +323,25 @@ elabPE info fc caller r =
323323 logLvl 3 $ "PE definition type : " ++ (show specTy)
324324 ++ "\n" ++ show opts
325325 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++
326−-- showSep "\n"
326+-- showSep "\n"
327327-- (map (\ (lhs, rhs) ->
328− (showTmImpls lhs ++ " = " ++
328+ (showTmImpls lhs ++ " = " ++
329329 showTmImpls rhs) -- pats)
330330
331331 logLvl 2 $ show n ++ " transformation rule: " ++
332332 show rhs ++ " ==> " ++ show lhs
333333
334334 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
335− let def = -- map (\ (lhs, rhs) ->
335+ let def = -- map (\ (lhs, rhs) ->
336336 [PClause fc newnm lhs [] rhs []] --) pats
337337 elabTransform info fc False rhs lhs
338338 elabClauses info fc opts newnm def)
339339 -- if it doesn't work, just don't specialise. Could happen for lots
340340 -- of valid reasons (e.g. local variables in scope which can't be
341341 -- lifted out).
342− (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))
342+ (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))
343343
344− specName (ImplicitS, tm)
344+ specName (ImplicitS, tm)
345345 | (P Ref n _, _) <- unApply tm = Just (n, Just 1)
346346 specName (ExplicitS, tm)
347347 | (P Ref n _, _) <- unApply tm = Just (n, Just 1)
@@ -370,8 +370,8 @@ elabPE info fc caller r =
370370
371371 -- get the clause of a specialised application
372372 getSpecClause ist (n, args)
373− = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++
374− qhash 0 (showSep "_" (map showArg args))) in
373+ = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++
374+ qhash 0 (showSep "_" (map showArg args))) in
375375 -- UN (show n ++ show (map snd args)) in
376376 (n, newnm, mkPE_TermDecl ist newnm n args)
377377 where showArg (ExplicitS, n) = show n
@@ -413,8 +413,8 @@ checkPossible info fc tcgen fname lhs_in
413413 validCase ctxt (Elaborating _ _ e) = validCase ctxt e
414414 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
415415 validCase ctxt _ = True
416−
417− recoverable ctxt (CantUnify r topx topy e _ _)
416+
417+ recoverable ctxt (CantUnify r topx topy e _ _)
418418 = let topx' = normalise ctxt [] topx
419419 topy' = normalise ctxt [] topy in
420420 checkRec topx' topy'
@@ -423,7 +423,7 @@ checkPossible info fc tcgen fname lhs_in
423423 recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e
424424 recoverable _ _ = False
425425
426− sameFam topx topy
426+ sameFam topx topy
427427 = case (unApply topx, unApply topy) of
428428 ((P _ x _, _), (P _ y _, _)) -> x == y
429429 _ -> False
@@ -434,11 +434,11 @@ checkPossible info fc tcgen fname lhs_in
434434
435435 checkRec (App f a) p@(P _ _ _) = checkRec f p
436436 checkRec p@(P _ _ _) (App f a) = checkRec p f
437− checkRec fa@(App _ _) fa'@(App _ _)
437+ checkRec fa@(App _ _) fa'@(App _ _)
438438 | (f, as) <- unApply fa,
439439 (f', as') <- unApply fa'
440− = if (length as /= length as')
441− then checkRec f f'
440+ = if (length as /= length as')
441+ then checkRec f f'
442442 else checkRec f f' && and (zipWith checkRec as as')
443443 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
444444 checkRec _ _ = False
@@ -488,7 +488,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
488488 let lhs = addImpl i lhs_in
489489 b <- checkPossible info fc tcgen fname lhs_in
490490 case b of
491− True -> tclift $ tfail (At fc
491+ True -> tclift $ tfail (At fc
492492 (Msg $ show lhs_in ++ " is a valid case"))
493493 False -> do ptm <- mkPatTm lhs_in
494494 return (Left ptm, lhs)
@@ -541,9 +541,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
541541 -- These are the names we're not allowed to use on the RHS, because
542542 -- they're UniqueTypes and borrowed from another function.
543543 -- FIXME: There is surely a nicer way than this...
544+ -- Issue #1615 on the Issue Tracker.
545+ -- https://github.com/idris-lang/Idris-dev/issues/1615
544546 when (not (null borrowed)) $
545547 logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)
546−
548+
547549 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
548550
549551 rep <- useREPL
@@ -587,7 +589,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
587589 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
588590 (do pbinds ist lhs_tm
589591 mapM_ setinj (nub (params ++ inj))
590− setNextName
592+ setNextName
591593 (_, _, is) <- errAt "right hand side of " fname
592594 (erun fc (build i winfo ERHS opts fname rhs))
593595 errAt "right hand side of " fname
@@ -604,7 +606,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
604606
605607 logLvl 5 "DONE CHECK"
606608 logLvl 2 $ "---> " ++ show rhs'
607− when (not (null defer)) $ iLOG $ "DEFERRED " ++
609+ when (not (null defer)) $ iLOG $ "DEFERRED " ++
608610 show (map (\ (n, (_,_,t)) -> (n, t)) defer)
609611 def' <- checkDef fc defer
610612 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
@@ -624,7 +626,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
624626 logLvl 5 $ "Rechecking"
625627 logLvl 6 $ " ==> " ++ show (forget rhs')
626628
627− (crhs, crhsty) <- if not inf
629+ (crhs, crhsty) <- if not inf
628630 then recheckC_borrowing True borrowed fc [] rhs'
629631 else return (rhs', clhsty)
630632 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
@@ -637,16 +639,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
637639 -- then we'll try running it in reverse to improve error messages
638640 let (ret_fam, _) = unApply (getRetTy crhsty)
639641 rev <- case ret_fam of
640− P _ rfamn _ ->
642+ P _ rfamn _ ->
641643 case lookupCtxt rfamn (idris_datatypes i) of
642− [TI _ _ dopts _ _] ->
644+ [TI _ _ dopts _ _] ->
643645 return (DataErrRev `elem` dopts)
644646 _ -> return False
645647 _ -> return False
646648
647649 when (rev || ErrorReverse `elem` opts) $ do
648650 addIBC (IBCErrRev (crhs, clhs))
649− addErrRev (crhs, clhs)
651+ addErrRev (crhs, clhs)
650652 return $ (Right (clhs, crhs), lhs)
651653 where
652654 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
@@ -666,7 +668,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
666668 -- we know they can't be used on the RHS
667669 borrowedNames :: [Name] -> Term -> [Name]
668670 borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)
669− | owner == txt "Ownership" &&
671+ | owner == txt "Ownership" &&
670672 (lend == txt "lend" || lend == txt "Read") = getVs arg
671673 where
672674 getVs (V i) = [env!!i]
@@ -714,7 +716,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
714716 isArg :: Name -> PDecl -> Bool
715717 isArg n (PClauses _ _ _ cs) = any isArg' cs
716718 where
717− isArg' (PClause _ _ (PApp _ _ args) _ _ _)
719+ isArg' (PClause _ _ (PApp _ _ args) _ _ _)
718720 = any (\x -> case x of
719721 PRef _ n' -> n == n'
720722 _ -> False) (map getTm args)
@@ -892,5 +894,3 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
892894 split deps [] pre = (reverse pre, [])
893895
894896 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
895−
896−