git.iko.soy/Idris-dev
on master help sign in
More information if a function is overapplied
commit6d768bb670db3b5ec17ab8655e9f581e71fb3f10 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 16 Mar 2015, 21:16 (12 years ago) parentebac088
5 files changed+19−1
compare with master
unifiedsplit
src/Idris/Core/Binary.hs+4 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/ProofState.hs+8−1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+5
src/Idris/Core/Binary.hs+4
@@ -29,6 +29,8 @@ instance Binary Provenance where
2929 put t
3030 put InferredVal = putWord8 2
3131 put GivenVal = putWord8 3
32+ put (TooManyArgs t) = do putWord8 4
33+ put t
3234
3335 get = do i <- getWord8
3436 case i of
@@ -37,6 +39,8 @@ instance Binary Provenance where
3739 return (SourceTerm x1)
3840 2 -> return InferredVal
3941 3 -> return GivenVal
42+ 4 -> do x1 <- get
43+ return (TooManyArgs x1)
4044 _ -> error "Corrupted binary data for Provenance"
4145
4246instance Binary a => Binary (Err' a) where
src/Idris/Core/DeepSeq.hs+1
@@ -48,6 +48,7 @@ instance NFData Provenance where
4848 rnf InferredVal = ()
4949 rnf GivenVal = ()
5050 rnf (SourceTerm x1) = rnf x1 `seq` ()
51+ rnf (TooManyArgs x1) = rnf x1 `seq` ()
5152
5253instance NFData Err where
5354 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) =
478478-- let valtyn = normalise ctxt env valty
479479-- let tyn = normalise ctxt env ty
480480 ns <- unify' ctxt env (valty, Just $ SourceTerm val)
481− (ty, Just ExpectedType)
481+ (ty, Just (chkPurpose val ty))
482482 ps <- get
483483 let (uh, uns) = unified ps
484484-- put (ps { unified = (uh, uns ++ ns) })
485485-- addLog (show (uh, uns ++ ns))
486486 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
487494fill _ _ _ _ = fail "Can't fill here."
488495
489496-- As fill, but attempts to solve other goals by matching
src/Idris/Core/TT.hs+1
@@ -121,6 +121,7 @@ data ErrorReportPart = TextPart String
121121-- Language.Reflection.Errors.Err in the stdlib!
122122
123123data Provenance = ExpectedType
124+ | TooManyArgs Term
124125 | InferredVal
125126 | GivenVal
126127 | SourceTerm Term
src/Idris/Delaborate.hs+5
@@ -202,6 +202,11 @@ pprintProv i e (SourceTerm tm)
202202 = text "Type of " <>
203203 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
204204 (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?"
205210
206211pprintErr :: IState -> Err -> Doc OutputAnnotation
207212pprintErr i err = pprintErr' i (fmap (errReverse i) err)