Pattern variables bound by type synonyms; or, how long is "due course" anyway?
If you compile the following code:
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
type ItemColID a b = Int -- Discards a,b
get :: ItemColID a b -> ItemColID a b
get (x :: ItemColID a b) = x :: ItemColID a b
Then surprisingly, GHC will reject it:
$ /opt/ghc/8.6.5/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:6: error:
• The type variables ‘a, b’
should be bound by the pattern signature ‘ItemColID a b’
but are actually discarded by a type synonym
To fix this, expand the type synonym
[Note: I hope to lift this restriction in due course]
• In the pattern: x :: ItemColID a b
In an equation for ‘get’:
get (x :: ItemColID a b) = x :: ItemColID a b
|
7 | get (x :: ItemColID a b) = x :: ItemColID a b
| ^^^^^^^^^^^^^^^^^^
Wow. The error message suggests that this restriction will be lifted in "due course". The funny thing is, this error message was added nine years ago in f670c47f? Surely that's long enough to constitute "due course"?
Indeed, if you look at #3406 (closed), the original issue which inspired this commit, @simonpj notes in #3406 (comment 35880) that "With the planned new "outside-in" type inference algorithm, however, this problem will go away." Well, OutsideIn(X) is certainly a thing now, so does that mean the problem really has gone away? I claim the answer is "yes", and there are two pieces of evidence to support this claim.
One piece of evidence is that if you switch ItemColID
from a type synonym to a type family, like so:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
type family ItemColID a b where ItemColID a b = Int -- Discards a,b
get :: ItemColID a b -> ItemColID a b
get (x :: ItemColID a b) = x :: ItemColID a b
Then GHC 8.6.5 is able to compile it without issue. You can see what happens at the Core level with -ddump-ds-preopt
:
$ /opt/ghc/8.6.5/bin/ghc Bug.hs -fforce-recomp -ddump-ds-preopt -dsuppress-coercions
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
==================== Desugar (before optimization) ====================
Result size of Desugar (before optimization)
= {terms: 15, types: 32, coercions: 26, joins: 0/2}
Rec {
-- RHS size: {terms: 5, types: 0, coercions: 0, joins: 0/0}
Bug.$trModule :: GHC.Types.Module
[LclIdX]
Bug.$trModule
= GHC.Types.Module
(GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Bug"#)
-- RHS size: {terms: 8, types: 21, coercions: 26, joins: 0/2}
get :: forall a b. ItemColID a b -> ItemColID a b
[LclIdX]
get
= \ (@ a_a16U) (@ b_a16V) (ds_d185 :: ItemColID a_a16U b_a16V) ->
let {
ds_d189 :: ItemColID GHC.Types.Any GHC.Types.Any
[LclId]
ds_d189 = ds_d185 `cast` <Co:13> } in
let {
x_aVQ :: ItemColID GHC.Types.Any GHC.Types.Any
[LclId]
x_aVQ = ds_d189 } in
x_aVQ `cast` <Co:13>
end Rec }
As you can see, a
and b
simply get instantiated in Any
, and everything works out fine.
The second piece of evidence is that I ripped out the code which throws the "I hope to lift this restriction in due course
" error message in GHC and ran the test suite, and all tests pass. The error message for T3406
changes slightly:
diff --git a/testsuite/tests/typecheck/should_fail/T3406.stderr b/testsuite/tests/typecheck/should_fail/T3406.stderr
index 4525bba5d6..69834d15f6 100644
--- a/testsuite/tests/typecheck/should_fail/T3406.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3406.stderr
@@ -1,10 +1,10 @@
-T3406.hs:11:6:
- The type variables ‘a, b’
- should be bound by the pattern signature ‘ItemColID a b’
- but are actually discarded by a type synonym
- To fix this, expand the type synonym
- [Note: I hope to lift this restriction in due course]
- In the pattern: x :: ItemColID a b
- In an equation for ‘get’:
- get (x :: ItemColID a b) = x :: ItemColID a b
+T3406.hs:11:28: error:
+ • Couldn't match type ‘Int’ with ‘a -> ItemColID a b’
+ Expected type: a -> ItemColID a b
+ Actual type: ItemColID a1 b1
+ • In the expression: x :: ItemColID a b
+ In an equation for ‘get’:
+ get (x :: ItemColID a b) = x :: ItemColID a b
+ • Relevant bindings include
+ get :: ItemColID a b -> a -> ItemColID a b (bound at T3406.hs:11:1)
But that is to be expected.
In light of this, is the time for "due course" now?