cogent
cogent copied to clipboard
au-ts
Pattern match failure in do expression
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
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 )
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.
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}
@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;
It doesn't crash though , right? Minigent doesn't try to generate a tree-structured typing proof.
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.
well, that'd get fixed once you enforce the !-ed thing to be used in the rhs I guess.
This issue seems to be the same issue #399, which has been solved by detecting it by the type checker.
