Changes between Version 22 and Version 23 of Records/OverloadedRecordFields/Implementation


Ignore:
Timestamp:
Aug 2, 2013 9:35:49 AM (2 years ago)
Author:
adamgundry
Comment:

GADT record updates make my brain hurt

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Implementation

    v22 v23  
    121121== GADT record updates ==
    122122
    123 Annoyingly, the generated code for `setField` doesn't typecheck for GADTs, because of #2595. At the moment, it generates
     123Annoyingly, the generated code for `setField` doesn't typecheck for GADTs, because of #2595. Consider the example
    124124
    125125{{{
     126data W a where
     127    MkW :: a ~ b => { x :: a, y :: b } -> W (a, b)
     128}}}
     129
     130At the moment, my code generates
     131
     132{{{
     133-- setField :: proxy "x" -> W (a, b) -> a -> W (a, b)
    126134setField _ s e = s { x = e }
    127135}}}
    128136
    129 for updating the field `x`, and this record update is rejected by the typechecker even though it is perfectly sensible. The alternative is to generate the rather long-winded explicit update
     137but this record update is rejected by the typechecker, even though it is perfectly sensible. The alternative is for me to generate the explicit update
    130138
    131139{{{
    132 setField _ (MkT1 f1 ... fi-1 _ fi+1 ... fn) e = MkT1 f1 ... fi-1 e fi+1 ... fn
    133 ...
    134 setField _ (MkTm ...)                       e = MkTm ...
     140setField _ (MkW _ y) x = MkW x y
    135141}}}
    136142
    137 I wonder if it would be easier to fix #2595.
     143which is fine, but rather long-winded if there are many constructors or fields. Essentially this is doing the job of the desugarer for record updates. I wonder if it would be easier to fix #2595. Perhaps not; the general case makes my brain hurt. I only need a rather special case: updating one field, where either the type does not change, or none of the local constraints mention changing type variables.
     144
     145Note that `W` does not admit type-changing single update for either field, because of the `a ~ b` constraint. Without it, though, type-changing update should be allowed.
    138146
    139147