search

willtim / Expresso

A simple expressions language with polymorphic extensible row types.
Other
300 stars 15 forks source link

Incomplete inferring for if expressions? #9

Closed FrankBro closed 5 years ago

FrankBro commented 6 years ago 
λ> let div = n d -> if d == 0 then DivBy0 {} else Ok (n / d)
λ> :type div
forall r. (r\Ok) => Int -> Int -> <DivBy0 : {}, Ok : Int | r>

Shouldn't the type of div be

forall r. (r\Ok\DivBy0) => Int -> Int -> <DivBy0 : {}, Ok : Int | r>

I noticed that if I swap Ok and DivBy0, I get

λ> let div = n d -> if d == 0 then Ok (n/d) else DivBy0 {}
λ> :type div
forall r. (r\DivBy0) => Int -> Int -> <Ok : Int, DivBy0 : {} | r>
willtim commented 6 years ago

Hi, I'm on holiday at the moment, but will try to take a look soon. This is indeed a bug and it was probably introduced by the rank-2 types support introduced by commit dedfae157. I will keep you posted!

willtim commented 6 years ago

Hi, I found the issue. If you look at line 164 in the file src/Expresso/Type.hs there is a TODO because I knew this line was wrong at the time I wrote it (I was intending to prune the substitution map elsewhere). If you change the line to read "Just t -> apply s t", the issue will be fixed. I will commit a proper fix when I get back from holiday and add some more tests. Many thanks!

willtim commented 6 years ago

I've committed a quick fix via the github web UI: https://github.com/willtim/Expresso/commit/ea82773874c7f4f1594a7becfcdc1c376660d92e

willtim commented 5 years ago

Test case for this pushed