Not in scope: type constructor or class ‘∼’-CodePudding

I'm trying to compile a code snippet from Maguire's Thinking with Types:

{-# LANGUAGE TypeOperators #-}

data Expr_ a
    = (a ∼ Int) => LitInt_ Int
    | (a ∼ Bool) => LitBool_ Bool
    | (a ∼ Int) => Add_ (Expr_ Int) (Expr_ Int)
    | (a ∼ Bool) => Not_ (Expr_ Bool)
    | If_ (Expr_ Bool) (Expr_ a) (Expr_ a)

Using GHCi, version 8.10.4, I get the following:

λ> :l TypeEquality.hs 
[1 of 1] Compiling Main             ( TypeEquality.hs, interpreted )

TypeEquality.hs:4:10: error:
    Not in scope: type constructor or class ‘∼’
  |
4 |     = (a ∼ Int) => LitInt_ Int
  |          ^

TypeEquality.hs:5:10: error:
    Not in scope: type constructor or class ‘∼’
  |
5 |     | (a ∼ Bool) => LitBool_ Bool
  |          ^

TypeEquality.hs:6:10: error:
    Not in scope: type constructor or class ‘∼’
  |
6 |     | (a ∼ Int) => Add_ (Expr_ Int) (Expr_ Int)
  |          ^

TypeEquality.hs:7:10: error:
    Not in scope: type constructor or class ‘∼’
  |
7 |     | (a ∼ Bool) => Not_ (Expr_ Bool)
  |          ^
Failed, no modules loaded.

Is there a language pragma that will make this compile?

CodePudding user response：

The real problem was that I had copy-and-pasted the code from the book, and the ~ symbol was formatted as the similar-but-not-identical ∼! I probably won't be the last person to make this mistake, so hopefully a search for the error message will bring someone to this post.

The following will compile:

{-# LANGUAGE GADTs #-}

data Expr_ a
    = (a ~ Int) => LitInt_ Int
    | (a ~ Bool) => LitBool_ Bool
    | (a ~ Int) => Add_ (Expr_ Int) (Expr_ Int)
    | (a ~ Bool) => Not_ (Expr_ Bool)
    | If_ (Expr_ Bool) (Expr_ a) (Expr_ a)