Why can't I match type Int with type a

December 27, 2021

Haskell Noob here.

An oversimplified case of what I’m trying to do here:

test :: Int -> a
test i = i -- Couldn't match expected type ‘a’ with actual type ‘Int’. ‘a’ is a rigid type variable bound by ...

I don’t quite understand why this wouldn’t work. I mean, Int is surely included in something of type a.

What I was really trying to achieve is this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data EnumType = Enum1 | Enum2 | Enum3

data MyType (a :: EnumType) where
  Type1 :: Int -> MyType 'Enum1
  Type2 :: String -> MyType 'Enum2
  Type3 :: Bool -> MyType 'Enum3

myFunc :: EnumType -> MyType 'Enum1 -> MyType any
myFunc Enum1 t = t -- Can't match type `any` with `Enum1`. any is a rigid type variable bound by ...
myFunc Enum2 _ = Type2 "hi"
myFunc Enum3 _ = Type3 True

What is going on here? Is there a way to work around this or is it just something you can’t do?

>Solution :

For the GADT function you want to write, the standard technique is to use singletons. The problem is that values of type EnumType are value-level things, but you want to inform the type system of something. So you need a way to connect types of kind EnumType with values of type EnumType (which itself has kind Type). That’s impossible, so we cheat: we connect types x of kind EnumType with values of a new type, SEnumType x, such that the value uniquely determines x. Here’s how it looks:

data SEnumType a where
    SEnum1 :: SEnumType Enum1
    SEnum2 :: SEnumType Enum2
    SEnum3 :: SEnumType Enum3

myFunc :: SEnumType a -> MyType Enum1 -> MyType a
myFunc SEnum1 t = t
myFunc SEnum2 _ = Type2 "hi"
myFunc SEnum3 _ = Type3 True

Now the a in the return type MyType a isn’t just fabricated out of thin air; it is constrained to be equal to the incoming a from SEnumType, and pattern matching on which SEnumType it is lets you observe whether a is Enum1, Enum2, or Enum3.