git.iko.soy/Idris-dev
on master help sign in
Be more careful with implicit FCs
5cb8ec3David Raymond Christiansen
src/Idris/AbsSyntax.hs+3−3
compare with master
unifiedsplit
@@ -1628,14 +1628,14 @@ addImpl' inpat env infns imp_meths ist ptm
1628aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[T.Text]] -> [PArg] -> Either Err PTerm
1628aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[T.Text]] -> [PArg] -> Either Err PTerm
1629aiFn inpat True qq imp_meths ist fc f ffc ds []
1629aiFn inpat True qq imp_meths ist fc f ffc ds []
1630 = case lookupDef f (tt_ctxt ist) of
1630 = case lookupDef f (tt_ctxt ist) of
1631− [] -> Right $ PPatvar fc f
1631+ [] -> Right $ PPatvar ffc f
1632 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1632 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1633 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1633 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1634 if (not (vname f) || tcname f
1634 if (not (vname f) || tcname f
1635 || any (conCaf (tt_ctxt ist)) ialts)
1635 || any (conCaf (tt_ctxt ist)) ialts)
1636-- any constructor alts || any allImp ialts))
1636-- any constructor alts || any allImp ialts))
1637− then aiFn inpat False qq imp_meths ist fc f fc ds [] -- use it as a constructor
1637+ then aiFn inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1638− else Right $ PPatvar fc f
1638+ else Right $ PPatvar ffc f
1639 where imp (PExp _ _ _ _) = False
1639 where imp (PExp _ _ _ _) = False
1640 imp _ = True
1640 imp _ = True
1641-- allImp [] = False
1641-- allImp [] = False
src/Idris/Elab/Term.hs+3−3
@@ -499,7 +499,7 @@ elab ist info emode opts fn tm
499 bindable (NS _ _) = False
499 bindable (NS _ _) = False
500 bindable (UN xs) = True
500 bindable (UN xs) = True
501 bindable n = implicitable n
501 bindable n = implicitable n
502− elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])
502+ elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp NoFC f [])
503 elab' ina fc' tm@(PRef fc n)
503 elab' ina fc' tm@(PRef fc n)
504 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
504 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
505 && isTConName n (tt_ctxt ist)
505 && isTConName n (tt_ctxt ist)
@@ -861,10 +861,10 @@ elab ist info emode opts fn tm
861 setInjective (PApp _ (PRef _ n) _) = setinj n
861 setInjective (PApp _ (PRef _ n) _) = setinj n
862 setInjective _ = return ()
862 setInjective _ = return ()
863
863
864− elab' ina _ tm@(PApp fc f [arg]) =
864+ elab' ina _ tm@(PApp fc f [arg]) =
865 erun fc $
865 erun fc $
866 do simple_app (not $ headRef f)
866 do simple_app (not $ headRef f)
867− (elabE (ina { e_isfn = True }) (Just fc) f)
867+ (elabE (ina { e_isfn = True }) (Just fc) f)
868 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
868 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
869 (show tm)
869 (show tm)
870 solve
870 solve