Skip to content

Record updates for existential fields do not work + confusing error

It would appear that updating a field with an existentially quantified type does not work, when using the record update notation. Here is an example:

{-# Language GADTs #-} -- Only uses Existentials
  
data T where
  Str :: Show s => { field :: s } -> T

val1 :: T
val1 = Str { field = True }

{-
val2 :: T
val2 = val1 { field = 'a' }
  • Record update for insufficiently polymorphic field: field :: s
    • In the expression: val1 {field = 'a'}
      In an equation for ‘val2’: val2 = val1 {field = 'a'}
-}

manualUpdate :: Show s => T -> s -> T
manualUpdate (Str _) s = Str s

val3 :: T
val3 = manualUpdate val1 'a'

Is there a reason why this shouldn't work? I would imagine that we'd like the record update to behave just like manualUpdate in the example.

Also, the error seems quite odd: how can a field be "insufficiently polymorphic"? After all, it is ok to update completely monomorphic fields.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information