Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

type checking issue about Integer and sum

Open luochen1990 opened this issue 6 years ago • 1 comments

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)

luochen1990 avatar May 14 '19 12:05 luochen1990

But following test2 type checks, which is weird

test2 : IO ()
test2 = print $ sum (map getValue xs)

luochen1990 avatar May 14 '19 12:05 luochen1990