GitLab

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) => () -> ()
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^