Inconsistent results with inaccessible code due to (~) vs. (~~)
The following code typechecks:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
data T = (Int ~ Char) => MkT { fld :: Int }
$ /opt/ghc/8.6.3/bin/ghci Bug.hs
GHCi, version 8.6.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:7:32: warning: [-Winaccessible-code]
• Couldn't match type ‘Int’ with ‘Char’
Inaccessible code in
a pattern with constructor: MkT :: (Int ~ Char) => Int -> T,
in an equation for ‘fld’
• In the pattern: MkT {fld = fld}
In an equation for ‘fld’: fld MkT {fld = fld} = fld
|
7 | data T = (Int ~ Char) => MkT { fld :: Int }
| ^^^
It produces a warning, of course, since there's no way to ever actually invoke fld
.
The interesting part of this is that if you replace ~
with ~~
in this program, then GHC will switch from accepting to rejecting it:
data T = (Int ~~ Char) => MkT { fld :: Int }
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:10: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘MkT’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’
|
7 | data T = (Int ~~ Char) => MkT { fld :: Int }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This feels strangely inconsistent.
A similar phenomenon occurs in function definitions. This function is accepted (with no warnings):
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
f :: (Int ~ Char) => () -> ()
f () = ()
But it is no longer accepted when ~
is swapped out with ~~
:
f :: (Int ~~ Char) => () -> ()
f () = ()
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:6: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (Int ~~ Char) => () -> ()
|
7 | f :: (Int ~~ Char) => () -> ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^