GHCi infers too-general type when pattern-matching on existential GADT
Run the following in ghci, I tested with version 8.8.3:
ghci -ghci-script Test.hs
:set -XGADTs
:set -XScopedTypeVariables
-- standard GADT with restricted type param
data X a where X :: X Int; XB :: X Bool
-- =============================================================================
-- standard ADT with full type params
data Pair0 a b t = Pair0 (a t) (b t)
Pair0 X x <- pure (Pair0 X [])
:t x
-- x :: [Int] as expected
x /= [10]
-- True
-- as expected, type inference matches x with [10]
-- =============================================================================
-- existential ADT, same as DSum from Data.Dependent.Sum
data Pair a b = forall t. Pair (a t) (b t)
-- same results with this equivalent GADT-syntax definition:
-- data Pair a b where Pair :: a t -> b t -> Pair a b
Pair X x <- pure (Pair X [])
x /= [10]
-- somehow, type inference fails to match x with [10]
-- • Couldn't match expected type ‘x’ with actual type ‘Integer’
:t x
-- x :: [t] but it should be
-- x :: [Int] because of the Pair X
--------------------------------------------------------------------------------
Pair X (x :: [Int]) <- pure (Pair X [])
x /= [10]
-- True
-- giving an explicit type signature fixes inference
--------------------------------------------------------------------------------
Pair X x <- pure (Pair X [0])
x /= [10]
-- True
-- giving an explicit value [0] also fixes inference
--------------------------------------------------------------------------------
:{
test :: IO ()
test = do
Pair X x <- pure (Pair X [])
print (x /= [10])
:}
test
-- True
-- putting the code inside a function, also fixes inference??
:{
test1 :: IO (Pair X [])
test1 = pure (Pair X [])
test2 :: Pair X [] -> IO ()
test2 (Pair X x) = print (x /= [10])
:}
test1 >>= test2
-- True
-- separating the functions also works, and we never hint x's type
I think this is different from #2206 (closed) and #14065 (closed) since the error message here is a pretty generic "Couldn't match type" rather than the GADT-specific error messages in those tickets ("GADT pattern match with non-rigid result type", "untouchable inside the constraints"), and it only affects GHCi.