Avoiding partial pattern matches using type-level metadata

[cocreature]

Let’s say I have the following fieldNames function which gives me back a list of the names of record fields:

{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, ScopedTypeVariables, TypeOperators #-}
module PartialSOP
  ( fieldNames
  ) where

import           GHC.TypeLits
import           Generics.SOP
import qualified Generics.SOP.Type.Metadata as T

fieldNames :: forall a proxy modName tyName constrName fields.
  ( Generic a
  , HasDatatypeInfo a
  , KnownSymbol modName
  , KnownSymbol tyName
  , DatatypeInfoOf a ~ 'T.ADT modName tyName '[ 'T.Record constrName fields]
  ) => proxy a -> [String]
fieldNames proxy =
  case datatypeInfo proxy of
    ADT _modName _tyName constrInfos ->
      case constrInfos of
        (constr :* Nil) ->
          case constr of
            Record _name fields ->
              let f :: forall f. FieldInfo f -> K String f
                  f (FieldInfo name) = K name
              in hcollapse (hliftA f fields)

This seems to work just fine and the equality constraint on DatatypeInfoOf should prevent users from using it on non-record types. However, datatypeInfo is giving me the term-level metadata and at that point I’ve lost all info about the metadata so GHC rightfully complains that the pattern matches are partial. I can convince it that the pattern match on constrInfos is not partial using a Code a ~ '[r] constraint (where r is a fresh type variable) but I’m failing to do something similar for the other two pattern matches.

It seems like convincing GHC that this is safe would require some kind of GADT which includes metadata. Does something like this already exist? If not have you thought about adding this? I haven’t tried creating one so far so I don’t know what problems will result from them but if you’re open to adding it I’ll give it a shot.

[kosmikus]

I'm honestly not entirely sure what the best way of working with type-level metadata is in general, but I think it's probably best to not use term-level metadata in combination with type-level metadata, and instead rather get all you want from the type-level metadata.

Your function could be written as follows:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Fieldnames where

import Generics.SOP
import qualified Generics.SOP.Type.Metadata as T
import GHC.TypeLits

fieldInfos ::
  forall a xs fields _m _d _c .
  ( Generic a
  , Code a ~ '[ xs ]
  , DatatypeInfoOf a ~ T.ADT _m _d '[ T.Record _c fields ]
  , T.DemoteFieldInfos fields xs
  ) => Proxy a -> NP FieldInfo xs
fieldInfos _ = T.demoteFieldInfos (Proxy @fields)

fieldNames ::
  forall a xs fields _m _d _c .
  ( Generic a
  , Code a ~ '[ xs ]
  , DatatypeInfoOf a ~ T.ADT _m _d '[ T.Record _c fields ]
  , T.DemoteFieldInfos fields xs
  ) => Proxy a -> NP (K String) xs
fieldNames = hmap (K . fieldName) . fieldInfos

I think these specific functions should probably be provided by the library even, along with a nicer type synonym capturing the constraint that something is a record type.

The GADT you suggest is another possibility, but I'm slightly reluctant to add yet another version of metadata. We have term-level metadata indexed by code, and type-level metadata already. And we'd then add another term-level metadata indexed by type-level metadata. I'm afraid this will become even more confusing to use.

[cocreature]

Thanks, I finally figured out how to get that info from the typelevelinfo thanks to your example! I agree that adding yet another version of metadata is probably not worth the cost so I’m closing this issue since using the typelevel metadata directly removes the need for partial pattern matches.