GitLab

I've been running into a few issues with partial type signatures as of late.

In my graphics shader library, users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.

However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.

After a fair bit of effort, I've finally managed to come up with a small reproducer:

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module Bug where

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

class C a where
  methC :: a -> Float
class D a where
  methD :: a -> Float

foo :: forall bool a. _ => SBool bool -> a -> Float
foo sBool a = meth a
  where
    meth :: _ => a -> Float
    meth = case sBool of
      STrue  -> methC 
      SFalse -> methD

produces the following error:

[1 of 1] Compiling Bug              ( bug.hs, bug.o )

bug.hs:23:17: error:
    * Could not deduce (C a) arising from a use of `methC'
      from the context: bool ~ 'True
        bound by a pattern with constructor: STrue :: SBool 'True,
                 in a case alternative
        at bug.hs:23:7-11
      Possible fix:
        add (C a) to the context of
          the inferred type of foo :: SBool bool -> a -> Float
    * In the expression: methC
      In a case alternative: STrue -> methC
      In the expression:
        case sBool of
          STrue -> methC
          SFalse -> methD
   |
23 |       STrue  -> methC
   |                 ^^^^^

bug.hs:24:17: error:
    * Could not deduce (D a) arising from a use of `methD'
      from the context: bool ~ 'False
        bound by a pattern with constructor: SFalse :: SBool 'False,
                 in a case alternative
        at bug.hs:24:7-12
      Possible fix:
        add (D a) to the context of
          the inferred type of foo :: SBool bool -> a -> Float
    * In the expression: methD
      In a case alternative: SFalse -> methD
      In the expression:
        case sBool of
          STrue -> methC
          SFalse -> methD
   |
24 |       SFalse -> methD
   |                 ^^^^^

If one follows the error messages that GHC provides, by adding the constraint ( C a, D a ) to meth, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses methC in both branches. If one changes SBool to Bool then of course it works fine.

I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves bool), i.e. it's as if we had just matched on a Bool.

---

Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).