179c704 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Record provenance of types in 'fill' errors

This covers unification errors arising from variables and function applications (which is a lot of them)

commit179c7043628c25807fed45c717cd1bc606057b20 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 16 Mar 2015, 18:27 (12 years ago) parent9546bd4

12 files changed+56−18

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/Core/Binary.hs+12 src/Idris/Core/DeepSeq.hs+4 src/Idris/Core/ProofState.hs+2−1 src/Idris/Core/TT.hs+7−1 src/Idris/Delaborate.hs+15−2 test/basic006/expected+2−2 test/proof002/expected+2−2 test/reg007/expected+2−2 test/reg023/expected+2−2 test/reg044/expected+2−2 test/tutorial006/expected+4−4

CHANGELOG+2

@@ -24,6 +24,8 @@ New in 0.9.17:

2424 called from foreign code

2525* Instances can now have documentation strings.

2626* Type providers can have documentation strings.

27+* Unification errors now (where possible) contain information about provenance

28+ of a type

2729

2830New in 0.9.16:

2931--------------

src/Idris/Core/Binary.hs+12

@@ -23,6 +23,18 @@ instance Binary ErrorReportPart where

2323 3 -> fmap SubReport get

2424 _ -> error "Corrupted binary data for ErrorReportPart"

2525

26+instance Binary Provenance where

27+ put ExpectedType = putWord8 0

28+ put (SourceTerm t) = do putWord8 1

29+ put t

30+

31+ get = do i <- getWord8

32+ case i of

33+ 0 -> return ExpectedType

34+ 1 -> do x1 <- get

35+ return (SourceTerm x1)

36+ _ -> error "Corrupted binary data for Provenance"

37+

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

2739 put (Msg str) = do putWord8 0

2840 put str

src/Idris/Core/DeepSeq.hs+4

@@ -43,6 +43,10 @@ instance NFData Raw where

4343instance NFData FC where

4444 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

4545

46+instance NFData Provenance where

47+ rnf ExpectedType = ()

48+ rnf (SourceTerm x1) = rnf x1 `seq` ()

49+

4650instance NFData Err where

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

4852 rnf (InternalMsg x1) = rnf x1 `seq` ()

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

@@ -477,7 +477,8 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

477477 do (val, valty) <- lift $ check ctxt env guess

478478-- let valtyn = normalise ctxt env valty

479479-- let tyn = normalise ctxt env ty

480− ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)

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

481+ (ty, Just ExpectedType)

481482 ps <- get

482483 let (uh, uns) = unified ps

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

src/Idris/Core/TT.hs+7−1

@@ -120,7 +120,13 @@ data ErrorReportPart = TextPart String

120120-- Please remember to keep Err synchronised with

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

122122

123−type Provenance = String

123+data Provenance = ExpectedType

124+ | SourceTerm Term

125+ deriving (Show, Eq, Data, Typeable)

126+{-!

127+deriving instance NFData Err

128+deriving instance Binary Err

129+!-}

124130

125131-- | Idris errors. Used as exceptions in the compiler, but reported to users

126132-- if they reach the top level.

src/Idris/Delaborate.hs+15−2

@@ -190,6 +190,11 @@ pprintTerm ist = pprintTerm' ist []

190190pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

191191pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

192192

193+pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation

194+pprintProv i e ExpectedType = text "Expected type"

195+pprintProv i e (SourceTerm tm)

196+ = text "Type of " <> pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm)

197+

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

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

195200

@@ -204,10 +209,18 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

204209 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

205210 text "Can't unify" <> indented (annTm x_ns

206211 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

207− ++ zip nms (repeat False)) x)) <$>

212+ ++ zip nms (repeat False)) x))

213+ <> case xprov of

214+ Nothing -> empty

215+ Just t -> text " (" <> pprintProv i sc t <> text ")"

216+ <$>

208217 text "with" <> indented (annTm y_ns

209218 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

210− ++ zip nms (repeat False)) y)) <>

219+ ++ zip nms (repeat False)) y))

220+ <> case yprov of

221+ Nothing -> empty

222+ Just t -> text " (" <> pprintProv i sc t <> text ")"

223+ <>

211224 case e of

212225 Msg "" -> empty

213226 -- if the specific error is the same as the one we just printed,

test/basic006/expected+2−2

@@ -1,8 +1,8 @@

11test020a.idr:16:18:When elaborating right hand side of foo:

22When elaborating an application of function Prelude.List.reverse:

33 Can't unify

4− Vect n a

4+ Vect n a (Type of xs)

55 with

6− List a

6+ List a (Expected type)

77[3, 2, 1]

88"Number 42"

test/proof002/expected+2−2

@@ -1,9 +1,9 @@

11Reflect.idr:208:38:When elaborating right hand side of testReflect1:

22When elaborating an application of function Reflect.getJust:

33 Can't unify

4− IsJust (Just x1)

4+ IsJust (Just x1) (Type of ItIsJust)

55 with

6− IsJust (prove (getProof x))

6+ IsJust (prove (getProof x)) (Expected type)

88 Specifically:

99 Can't unify

test/reg007/expected+2−2

@@ -1,9 +1,9 @@

11reg007.lidr:8:1:A.n is already defined

22reg007.lidr:12:11:When elaborating right hand side of hurrah:

33Can't unify

4− n = lala

4+ n = lala (Type of isSame)

55with

6− 0 = 1

6+ 0 = 1 (Expected type)

88Specifically:

99 Can't unify

test/reg023/expected+2−2

@@ -1,5 +1,5 @@

11reg023.idr:7:5:When elaborating right hand side of bad:

22Can't unify

3− [94mNat[0m

3+ [94mNat[0m (Type of [91m0[0m)

44with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m (Expected type)

test/reg044/expected+2−2

@@ -1,8 +1,8 @@

11reg044.idr:4:4:When elaborating right hand side of Main.pf:

22Can't unify

3− [95mb[0m [94m=[0m [95mb[0m

3+ [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

44with

5− [95ma[0m [94m=[0m [95mb[0m

5+ [95ma[0m [94m=[0m [95mb[0m (Expected type)

77Specifically:

88 Can't unify

test/tutorial006/expected+4−4

@@ -1,9 +1,9 @@

11tutorial006a.idr:5:23:When elaborating right hand side of vapp:

22When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

33 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp _ _)

55 with

6− [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m

6+ [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

88 Specifically:

99 Can't unify

@@ -12,9 +12,9 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

1212 [92mplus[0m [95mn[0m [95mm[0m

1313tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

1414Can't unify

15− [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

15+ [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

1616with

17− [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m)))

17+ [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

1818

1919Specifically:

2020 Can't unify