Guarding against errant field accessors/ record selectors

Consider

data W 
  = WithoutField
  | WithField with
      field : Int

getMyField : W -> Int
getMyField a = a.field

t :  Script ()
t  =  do

  let w = WithField 10

  debug $ getMyField w

  let wo = WithoutField
  debug $ getMyField wo

The code above compiles, but the script will fail with an error.

1. AFAIK, there’s no way to turn this into an error, and I can’t find a warning. Is that correct?
2. Is there any way to statically check for usage of missing record selectors? I know that I () would never write such code, so asking for a friend.

You are correct that there is no warning for this unfortunately and we don’t have any separate static checks for this either. Your best option is to not define those types in the first place and instead split your records and variants:

data W = WithoutField | WithField WithField

data WithField = WithFieldR with field : Int

Then you cannot use the field on the wrong constructor without getting a type error. Of course that just brings back the question of how you can enforce this …

Thank you.