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

CHANGELOG+2

compare with master

unifiedsplit

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

24 called from foreign code

25* Instances can now have documentation strings.

26* Type providers can have documentation strings.

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

28+ of a type

27

29

28New in 0.9.16:

30New in 0.9.16:

29--------------

31--------------

src/Idris/Core/Binary.hs+12

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

23 3 -> fmap SubReport get

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

25

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+

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

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

27 put (Msg str) = do putWord8 0

39 put (Msg str) = do putWord8 0

28 put str

40 put str

src/Idris/Core/DeepSeq.hs+4

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

43instance NFData FC where

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

45

46+instance NFData Provenance where

47+ rnf ExpectedType = ()

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

49+

46instance NFData Err where

50instance NFData Err where

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

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

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

52 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) =

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

478-- let valtyn = normalise ctxt env valty

479-- 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)

481 ps <- get

482 ps <- get

482 let (uh, uns) = unified ps

483 let (uh, uns) = unified ps

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

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

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

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

120-- Please remember to keep Err synchronised with

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

122

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+!-}

124

130

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

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

126-- if they reach the top level.

132-- if they reach the top level.

src/Idris/Delaborate.hs+15−2

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

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

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

192

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+

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

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

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

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

195

200

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

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

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

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

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

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

211 (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+ <$>

208 text "with" <> indented (annTm y_ns

217 text "with" <> indented (annTm y_ns

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

218 (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+ <>

211 case e of

224 case e of

212 Msg "" -> empty

225 Msg "" -> empty

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

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

test/basic006/expected+2−2

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

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

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

3 Can't unify

4− Vect n a

4+ Vect n a (Type of xs)

5 with

6− List a

6+ List a (Expected type)

7[3, 2, 1]

8"Number 42"

test/proof002/expected+2−2

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

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

2When elaborating an application of function Reflect.getJust:

3 Can't unify

4− IsJust (Just x1)

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

5 with

6− IsJust (prove (getProof x))

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

7

8 Specifically:

9 Can't unify

test/reg007/expected+2−2

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

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

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

3Can't unify

4− n = lala

4+ n = lala (Type of isSame)

5with

6− 0 = 1

6+ 0 = 1 (Expected type)

7

8Specifically:

9 Can't unify

test/reg023/expected+2−2

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

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

2Can't unify

3− [94mNat[0m

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

4with

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

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

test/reg044/expected+2−2

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

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

2Can't unify

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

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

4with

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

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

6

7Specifically:

8 Can't unify

test/tutorial006/expected+4−4

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

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

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

3 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 _ _)

5 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)

7

8 Specifically:

9 Can't unify

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

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

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

14Can'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)

16with

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)

18

19Specifically:

20 Can't unify