'Why can't I match type Int with type a

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?

haskell


Solution 1:[1]

Is there a way to work around this or is it just something you can't do?

I'm afraid that it's just "something you can't do". The reason is simple to explain.

When you write a type signature like (to take your first, simpler example)

test :: Int -> a

or, to write it the more literal, expanded form

test :: forall a. Int -> a

You are saying that literally, "for all a", this function can take an Int and return a value of type a. This is important, because calling code has to believe this type signature and therefore be able to do something like this (this isn't realistic code, but imagine a case where you feed the result of test 2 to a function that requires a Char or one of those other types):

test 2 :: Char
test 2 :: [Int]
test 2 :: (Double, [Char])

and so on. Clearly your function can't work with any of these examples - but it has to be able to work with any of them if you give it this type signature. Your code, quite simply, does not fit that type signature. (And nor could any, unless you "cheat" by having eg test x = undefined.)

This shouldn't be a problem though - the compiler is simply protecting you from a mistake, because I'm sure you realise that your code cannot satisfy this type signature. To take your "real" example:

myFunc :: EnumType -> MyType Enum1 -> MyType any

although this produces a compilation error, your code in the function is likely correct, and the problem is the type signature. If you replace it with

myFunc :: EnumType -> MyType Enum1 -> MyType Enum1

then it will compile (barring any further errors, which I've not checked it for), and presumably do what you want. It doesn't look like you actually want to be able to call myFunc and have it produce, say, a MyType Int. (If by any chance you do, I'd suggest you ask a separate question where you elaborate on what you actually need here.)

Solution 2:[2]

As was already said, your signature expresses a universal type

myFunc :: ? a . EnumType -> MyType 'Enum1 -> MyType a

whereas what you're actually trying to express is an existential type

myFunc :: EnumType -> MyType 'Enum1 -> (? a . MyType a)

Haskell doesn't have a feature quite like that, but it does have some way to achieve essentially the same thing.

  1. Both GADTs and the ExistentialTypes extension allow expressing existentials, but you need to define a separate type for them.

    data MyDynType where
  MyDynWrap :: MyType a -> MyDynType

myFunc :: EnumType -> MyType 'Enum1 -> MyDynType
myFunc Enum1 t = MyDynWrap t
myFunc Enum2 _ = MyDynWrap $ Type2 "hi"
myFunc Enum3 _ = MyDynWrap $ Type3 True

  2. Maybe you don't even need a separate type, but can simply modify MyType to be “dynamic” in the first place.

    data MyType = Type1 Int | Type2 String | Type3 Bool

myFunc :: EnumType -> MyType -> MyType
myFunc Enum1 (Type1 i) = Type1 i
myFunc Enum2 _ = Type2 "hi"
myFunc Enum3 _ = Type3 True

  3. existentials can be emulated at the spot, anonymously, by unwrapping a layer of continuation-passing style and then using the dual universal quantifier via the RankNTypes extension.

    {-# LANGUAGE RankNTypes #-}

data MyType (a :: EnumType) where ... -- as original

myFunc :: EnumType -> MyType 'Enum1 -> (? a . MyType a -> r) -> r
myFunc Enum1 t q = q t
myFunc Enum2 _ q = q (Type2 "hi")
myFunc Enum3 _ q = q (Type3 True)

Solution 3:[3]

the GADT function you want to write, the standard technique is to use singletons. The problem is that values of type EnumType are website...

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Robin Zigmond
Solution 2 leftaroundabout
Solution 3

Related Questions