Type equality constraints syntax

Learn
#1

Hi,

I’m reading this entry: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/data_kinds.html#overview
And I understand tilde stands for a constraint that types a and Int must be equal, but what does double tilde stand for MkFoo2 :: a ~~ Int ?

Also, in this particular scenario (matching types in GADTs) is there any practical difference between

MkFoo1 :: a ~ Int => ...
and
MkFoo1 :: a ~~ Int => ...
?

#2

You can find it with hoogle: https://hoogle.haskell.org/?hoogle=~~. Here is the documentation: https://hackage.haskell.org/package/ghc-prim-0.6.1/docs/GHC-Types.html#t:-126--126-

I don’t have much experience with it, but here is an example of how they differ:

> :k Eq ~ Int

<interactive>:1:6: error:
    • Expected kind ‘* -> Constraint’, but ‘Int’ has kind ‘*’
    • In the second argument of ‘(~)’, namely ‘Int’
      In the type ‘Eq ~ Int’
> :k Eq ~~ Int
Eq ~~ Int :: Constraint

So you can use ~~ with types that have different kinds.

The second example MkFoo1 :: Int => ... doesn’t make sense to me, because Int is a type and not a constraint, so it cannot appear on its own on the left of the constraint arrow =>. You will get an error:

> :k Int => Int

<interactive>:1:1: error:
    • Expected a constraint, but ‘Int’ has kind ‘*’
    • In the type ‘Int => Int’

Edit: Oh, I think you meant a ~~ Int => ..., in that case there is no real difference in that particular example, but you can write more things, like:

> :set -XTypeOperators
> :set -XTypeFamilies
> :set -XKindSignatures
> :set -XExplicitForAll
> import GHC.Types
> :k forall (a :: *). a ~ Eq => a

<interactive>:1:22: error:
    • Expecting one more argument to ‘Eq’
      Expected a type, but ‘Eq’ has kind ‘* -> Constraint’
    • In the second argument of ‘(~)’, namely ‘Eq’
      In the type ‘forall (a :: *). a ~ Eq => a’
> :k forall (a :: *). a ~ Eq => a
forall (a :: *). a ~~ Eq => a :: *

I would have expected to be able to write:

{-# LANGUAGE TypeOperators, TypeFamilies, ExplicitForAll, KindSignatures #-}

import GHC.Types

x :: forall (a :: *). a ~~ Eq => a
x = undefined

But, I’m getting an error:

[1 of 1] Compiling Main             ( Test.hs, interpreted )

Test.hs:5:6: error:
    • Couldn't match kind ‘* -> Constraint’ with ‘*’
      When matching types
        a :: *
        Eq :: * -> Constraint
    • In the ambiguity check for ‘x’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: x :: forall (a :: *). a ~~ Eq => a
  |
5 | x :: forall (a :: *). a ~~ Eq => a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I’ve opened a GHC issue: https://gitlab.haskell.org/ghc/ghc/-/issues/19560

1 Like
#3

yes I did mean a ~~ Int, thanks!