Pattern match failure in do expression

[kai-e]

cogent -g fails on

type RS s = < Continue s >
type World
type Array x
array_bget : all x. ((Array x)!, U32) -> x

type Ra = #{ x : Array (U8), b : Bool }
type V = ()

type L_p = < L_p_4 >

type V_p = #{ hErp_pv_0 : U8, r : Ra }

delta_p : ( World, L_p, V_p ) -> ( World, V_p, RS L_p )
delta_p ( w, loc_p, #{ hErp_pv_0, r } ) =
  loc_p
  | L_p_4 -> ( w
             , #{ hErp_pv_0
                , r = r {b = if (let hErp_r = array_bget ( r.x, (0 : U32) ) !r in
                  hErp_r) == '0' then False else True} }
             , Continue L_p_4 )

with

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
cogent: Pattern match failure in do expression at src/Cogent/Inference.hs:353:9-14

[kai-e]

Lifting the binding prevents the error:

  | L_p_4 -> let hErp_r = array_bget ( r.x, (0 : U32) ) !r in
             ( w
             , #{ hErp_pv_0
                , r = r {b = if hErp_r == '0' then False else True} }
             , Continue L_p_4 )

[zilinc]

even smaller example:

type A
array_bget : all x. (A!, U32) -> x

type Ra = #{ x : A, b : Bool }

type L_p = < L_p_4 >

type V_p = #{ hErp_pv_0 : U8, r : Ra }

delta_p : Ra -> Ra 
delta_p r = r {b = let y = array_bget ( r.x, 0 : U32 ) !r in y}

We know the problem. I'll patch it sometime soon.

[kai-e]

It keeps shrinking.

type A
f : (A!) -> Bool
type R = #{ x : A, b : Bool }
g : R -> R 
g r = r {b = let y = f ( r.x ) !r in y}

[zilinc]

@liamoc seems that minigent has the same issue:

f : A! -> Bool;

g : { x : A, b : Bool }# -> { x : A, b : Bool }#;
g r = put r.b := let! (r) y = f (r.x) in y end end;

[liamoc]

It doesn't crash though , right? Minigent doesn't try to generate a tree-structured typing proof.

[zilinc]

no, but it doesn't reject the program.

[liamoc]

Right, that's expected behaviour, seeing as I don't check that you use let!'ed variables in the RHS. To be fully compliant with the typing rules, I should, but I didn't bother for now.

[zilinc]

Ok, but what about the fact that r is double-used in the put-expression?

[zilinc]

well, that'd get fixed once you enforce the !-ed thing to be used in the rhs I guess.

[gteege]

This issue seems to be the same issue #399, which has been solved by detecting it by the type checker.