Partial type signature algorithm fails to infer constraints in the presence of GADTs
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).