RAE_T32a.hs:29:1: error:
    • Expected kind ‘k -> *’, but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
    • In the data instance declaration for ‘Sing’

RAE_T32a.hs:29:20: error:
    • Expecting two more arguments to ‘Sigma’
      Expected a type, but
      ‘Sigma’ has kind
      ‘forall p -> TyPi p (MkStar p) -> *’
    • In the first argument of ‘Sing’, namely ‘Sigma’
      In the data instance declaration for ‘Sing’

RAE_T32a.hs:29:27: error:
    • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
    • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
      In the data instance declaration for ‘Sing’