Geek Answers Handbook

`zipWith (-) [6,5,4] [1,2,3]` errors

Why zipWith (-) [6,5,4] [1,2,3] n't zipWith (-) [6,5,4] [1,2,3] work in Idris? Can this error be avoided without writing a specialized zipWith function?

main8.idr:

 module Main import Data.HVect import Data.Vect import Data.Vect.Quantifiers t : Vect 3 Nat t = zipWith (-) [6,5,4] [1,2,3]

Mistake:

 *main8> :load main8.idr Type checking ./main8.idr main8.idr:8:3:When checking right hand side of t with expected type Vect 3 Nat When checking argument f to function Data.Vect.zipWith: Can't disambiguate since no name has a suitable type: Prelude.Interfaces.-, Prelude.Nat.- Holes: Main.t

This file works:

 module Main import Data.HVect import Data.Vect import Data.Vect.Quantifiers vm : (ms : Vect l Nat) -> (ns : Vect l Nat) -> {auto p : All (uncurry LTE) (zip ns ms)} -> Vect l Nat vm [] [] = [] vm {p = _ :: _} (m::ms) (n::ns) = m - n :: vm ms ns t : Vect 3 Nat t = vm [6,5,4] [1,2,3]
+7
idris
source share

No one has answered this question yet.

See related questions:

4
Strange error message with Idris interfaces
2
VerifiedMonad instance for monad error
2
Views in Idris - Listing 10.5 of the development based on type in Idris's book
one
Syntax error when using views
one
Strong syntax error
one
Idris - expression does not check type when importing from module
0
Compilation error while implementing extensible record
0
Idris implies the error message "... is not an implicit argument ..."
0
concat in zipWith "there is no such variable a"
0
Unable to override name: Prelude.List. ++, Prelude.Strings. ++ bug in Idris

More articles:


All Articles