Idris-dev
Idris-dev copied to clipboard
type checking issue about Integer and sum
Steps to Reproduce
data TyRep = Number | Text
data Value : TyRep -> Type where
NumberV : Int -> Value Number
TextV : String -> Value Text
valueRep : TyRep -> Type
valueRep tr = case tr of
Number => Int
Text => String
getValue : {t : TyRep} -> Value t -> valueRep t
getValue {t} v = case (t, v) of
(Number, NumberV x) => x
(Text, TextV s) => s
xs : List (Value Number)
xs = [NumberV (the Int 1), NumberV (the Int 2)]
test : IO ()
test = print (sum $ map (\(NumberV x) => x) xs)
Expected Behavior
test type checks
Observed Behavior
Following error is reported:
|
21 | test = print (sum $ map (\(NumberV x) => x) xs)
| ^
...
Type mismatch between
Int (Type of x)
and
Integer (Expected type)
But following test2 type checks, which is weird
test2 : IO ()
test2 = print $ sum (map getValue xs)