6d768bb · Idris-dev · git.iko.soy

src/Idris/Core/Binary.hs+4

compare with master

unifiedsplit

@@ -29,6 +29,8 @@ instance Binary Provenance where

29 put t

30 put InferredVal = putWord8 2

31 put GivenVal = putWord8 3

32+ put (TooManyArgs t) = do putWord8 4

33+ put t

32

34

33 get = do i <- getWord8

35 get = do i <- getWord8

34 case i of

36 case i of

@@ -37,6 +39,8 @@ instance Binary Provenance where

37 return (SourceTerm x1)

39 return (SourceTerm x1)

38 2 -> return InferredVal

40 2 -> return InferredVal

39 3 -> return GivenVal

41 3 -> return GivenVal

42+ 4 -> do x1 <- get

43+ return (TooManyArgs x1)

40 _ -> error "Corrupted binary data for Provenance"

44 _ -> error "Corrupted binary data for Provenance"

41

45

42instance Binary a => Binary (Err' a) where

46instance Binary a => Binary (Err' a) where

src/Idris/Core/DeepSeq.hs+1

@@ -48,6 +48,7 @@ instance NFData Provenance where

48 rnf InferredVal = ()

49 rnf GivenVal = ()

50 rnf (SourceTerm x1) = rnf x1 `seq` ()

51+ rnf (TooManyArgs x1) = rnf x1 `seq` ()

51

52

52instance NFData Err where

53instance NFData Err where

53 rnf (Msg x1) = rnf x1 `seq` ()

54 rnf (Msg x1) = rnf x1 `seq` ()

src/Idris/Core/ProofState.hs+8−1

@@ -478,12 +478,19 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

478-- let valtyn = normalise ctxt env valty

479-- let tyn = normalise ctxt env ty

480 ns <- unify' ctxt env (valty, Just $ SourceTerm val)

481− (ty, Just ExpectedType)

481+ (ty, Just (chkPurpose val ty))

482 ps <- get

483 let (uh, uns) = unified ps

484-- put (ps { unified = (uh, uns ++ ns) })

485-- addLog (show (uh, uns ++ ns))

486 return $ Bind x (Guess ty val) sc

487+ where

488+ -- some expected types show up commonly in errors and indicate a

489+ -- specific problem.

490+ -- argTy -> retTy suggests a function applied to too many arguments

491+ chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))

492+ = TooManyArgs val

493+ chkPurpose _ _ = ExpectedType

487fill _ _ _ _ = fail "Can't fill here."

494fill _ _ _ _ = fail "Can't fill here."

488

495

489-- As fill, but attempts to solve other goals by matching

496-- As fill, but attempts to solve other goals by matching

src/Idris/Core/TT.hs+1

@@ -121,6 +121,7 @@ data ErrorReportPart = TextPart String

121-- Language.Reflection.Errors.Err in the stdlib!

122

123data Provenance = ExpectedType

124+ | TooManyArgs Term

124 | InferredVal

125 | InferredVal

125 | GivenVal

126 | GivenVal

126 | SourceTerm Term

127 | SourceTerm Term

src/Idris/Delaborate.hs+5

@@ -202,6 +202,11 @@ pprintProv i e (SourceTerm tm)

202 = text "Type of " <>

203 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

204 (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

205+pprintProv i e (TooManyArgs tm)

206+ = text "Is " <>

207+ annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

208+ (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

209+ <> text " applied to too many arguments?"

205

210

206pprintErr :: IState -> Err -> Doc OutputAnnotation

211pprintErr :: IState -> Err -> Doc OutputAnnotation

207pprintErr i err = pprintErr' i (fmap (errReverse i) err)

212pprintErr i err = pprintErr' i (fmap (errReverse i) err)