Can I get GHC to infer a constraint past a GADT pattern match?

Question

I would like to get GHC to infer a constraint past a GADT pattern match. For instance, suppose I have two expressions, each with an inferred constraint:

f :: _ => a
g :: _ => a

(In my use case, these inferred constraints can be large, so it isn't feasible to write them out by hand.)

Suppose then that I want to use either f or g depending on a boolean conditional. Naively, I can proceed as follows:

h1 :: _ => Bool -> a
h1 c = if c then f else g

Supposing I call the inferred constraint for f ct_f and that for g ct_g, then GHC will infer the constraint ( ct_f, ct_g ) for h1.

The problem is that this is an overly restrictive type: if the Boolean is True I don't need ct_g, and conversely if it's False I don't need ct_f. So I attempt to use the standard machinery to enable such a dependent constraint:

data SBool (c :: Bool) where
  SFalse :: SBool False
  STrue  :: SBool True

h2 :: _ => SBool bool -> a
h2 = \case
  STrue  -> f
  SFalse -> g

However this doesn't work, as GHC's partial type signature algorithm refuses to float constraints past a GADT pattern match. Instead, I can try to tell GHC explicitly what to do:

ifC :: forall ct_t ct_f bool x. SBool bool -> ( ct_t => x ) -> ( ct_f => x ) -> ( If bool ct_t ct_f => x )
ifC STrue  a _ = a
ifC SFalse _ b = b

h3 :: _ => SBool bool -> a
h3 c = ifC c f g

This approach fails too, this time because GHC deems the type signature of ifC ambiguous, i.e. GHC needs the user to explicitly pass the constraints like

h4 c = ifC @ct_f @ct_g c f g

Unfortunately, I can't explicitly pass these constraints: I am asking GHC to infer them, and have no way to refer to them. For instance, one might try to bring them in scope as follows:

h5 :: _ => SBool bool -> a
h5 c = 
  let
    f :: _ct_f => a
    f' = f
    g :: _ct_g => a
    g' = g
  in
    if_C @_ct_f @_ct_g c f' g'

But this can't work, as GHC doesn't support named wildcards standing in for extra constraints (and even if it did, they wouldn't scope correctly).

Is there another way to proceed which would allow GHC to infer:

h :: ( If bool ct_f ct_g ) => a

"I have no way to refer to them" did you mean you don't want to refer to those constraints explicitly as a matter of design, or is there some other obstacle? — Li-yao Xia
I think the core problem here is this: constraints are never unified with each other. That seems pretty damning for any attempt to do this. — Daniel Wagner
+1 for a a thought-provoking question, but honestly I think the whole approach is doomed. Typed holes can be convenient, sure, but I don't think it's smart to ever rely on them too much. — leftaroundabout

Akihito KIRISAKI Akihito KIRISAKI · Accepted Answer · 2020-12-17T15:54:23

I have improved code a little bit with ImpredicativeTypes.

type family GetBool a where
  GetBool (SBool True) = True 
  GetBool (SBool False) = False

data TF (a :: Constraint) x = TF x

class SIf a pt pf x where
  ifC' :: a -> TF pt x -> TF pf x -> (If (GetBool a) pt pf => x)

instance ((t => x) ~ (f => x)) => SIf (SBool True) t f x where
  ifC' _ (TF t) _ = t

instance ((t => x) ~ (f => x)) => SIf (SBool False) t f x where
  ifC' _ _ (TF f) = f

h3' :: _ => SBool bool -> a
h3' c = ifC' c f g

It works to give it Num a instance.

*Main> :t h3' 3
h3' 3
  :: (If (GetBool (SBool bool)) pt pf, SIf (SBool bool) pt pf a,
      Num (SBool bool)) =>
     a

let x = h3' f works too for now, but is not perfect. I suppose what we do is black magic...

Can I get GHC to infer a constraint past a GADT pattern match?

1 Answers