haskell type family result not matching

Question

I want to specify function result type based on the type of first argument. To define this dependecy I define type family MaybeWrapper. It wrap some result type in Maybe if first argument is Opt type (Optional). Opt and Req a singelton types. And I want them to define result type Opt - > Maybe v and Req -> v

Here the code:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Typeable
import Data.Type.Equality

-- singelton types:
data Opt = Opt deriving Show
data Req = Req deriving Show

type family MaybeWrapper a v where
    MaybeWrapper Opt v = Maybe v
    MaybeWrapper _ v = v


f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v
f1 a vv 
  | Just Refl <- eqT @a @Opt = Just vv
  | otherwise = vv

f2 :: a -> v -> MaybeWrapper a v
f2 Opt vv = Just vv
f2 _ vv = vv

But all my attemts 1 and 2 fail.

Error:

• Couldn't match expected type ‘MaybeWrapper a v’ with actual type ‘v’

I expect that "MaybeWrapper a v" is not a type but a type function which must resolve to v type with Opt argument and types must match.

How can I fix this?

Added:

So I found that i can fix it with typeclasses:

class CMaybe a where
  type MWrap a v 
  vf :: a -> v -> MWrap a v 

instance CMaybe Opt where
  type MWrap Opt v = Maybe v
  vf _ = Just 

instance CMaybe Req where
  type MWrap Req v = v
  vf _ v = v

But why haskell can't infer types without them here?

Answer 1

First, your second attempt is a complete non-starter. You simply cannot match a value whose type is simply a variable like a against a pattern for one specific type (such as Opt, which is a pattern for a type named Opt). There are loads of questions and answers on Stack Overflow going over this in more detail, so I won't elaborate here.

Your first attempt is more interesting, so let's consider why that doesn't work.

First, I hope it is obvious why this doesn't work:

f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v
f1 a vv = vv

When compiling the expression vv on the right hand side the compiler has no information about what type a is (or v for that matter). So when it looks at the definition of MaybeWrapper a v, it doesn't have any proof that a is Opt and thus cannot take the first branch and conclude that MaybeWrapper a v = Maybe v. But it also doesn't have any proof that a is not Opt; so it can't take the second branch either.

What it is left with is that the type of the right hand side is expected to be simply MaybeWrapper a v; with no information to go on it can't reduce the type family to any specific type. That's why you get an error like:

    • Couldn't match expected type ‘MaybeWrapper a v’
                  with actual type ‘v’

It's not saying that MaybeWrapper a v is some concrete type, it's saying it has no idea what concrete type that evaluates to so it cannot match anything else with it.

(If f1 took an argument that had type MaybeWrapper a v, it would be able to conclude that the argument value had the same type as the return value, and so you could return that even without reducing the type family. But you can't really do anything else with a value whose type is an unreduced type family)

So then we can look at your actual f1:

f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v
f1 a vv 
  | Just Refl <- eqT @a @Opt = Just vv
  | otherwise = vv

In the first branch, you use Typeable and eqT. This allows you to write a specific branch of the code where the compiler considers that it has evidence that a ~ Opt. This means that it can reduce MaybeWrapper a v to Maybe v, and so you can return Just vv on that branch. If you look carefully at the error message you get, you will see that it is not complaining about this line; the compiler is happy here.

But the additional evidence only applies inside the scope of the Just Refl pattern match. Outside the pattern match all the code must compile with the same total lack of any information about the type a. You might wish that being in a branch that could only be reached if eqT failed to match would give the compiler evidence of type inequality, but that's simply not how it works.

(When eqT tests the types and finds thay are equal, it gives you back Just Refl, where the Refl is a special value that provides evidence of type equality to the compiler. But when eqT finds the types aren't equal, it just gives you back Nothing, which doesn't contain any evidence the type checker can use; and you didn't even pattern match on it so you wouldn't have got the evidence even if it was there).

So you can sortof make your code work by using eqT again:

f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v
f1 a vv 
  | Just Refl <- eqT @a @Opt = Just vv
  | Just Refl <- eqT @a @Req = vv

Now both of your two branches are compiled with additional knowledge about the type of a. Knowing that a is Req is enough to reduce MaybeWrapper a v to v, so on that branch you can return vv as you wanted.

The problem with this is that now your guards are not exhaustive (and the compiler will warn you about this if you use -Wall). You know that you want this parameter to be Opt or Req, but what you've actually said is that it can be any type a that has a Typeable instance. Try writing a file where you call things like f1 True (), or f1 (putStrLn "whoops") (); the type checker will happily allow it, but running that code will fail at runtime with Non-exhaustive patterns in function f1. So this is not very type-safe.

A better way is to define Opt and Req together as the only possible members of a new kind, instead of defining them as separate types. Then you can define a GADT of singletons that provide the ability to pattern match on a value to find out whether a type parameter was Opt or Req (and disallow any other type). With that setup, all you need is regular pattern matching to do what you want; no Typeable or custom type class. It looks like this (compiles as-is with GHC 9.4.8; you might need to enable some more extensions in older versions):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind ( Type )


-- Optionality is an ordinary type, with Opt and Req as value
-- constructors. We're never going to use it like that, however. The
-- DataKinds extension will automatically allow us to use Opt and Req
-- as (uninhabited) types, with Optionality being a *kind* that allows
-- only those two types (a kind is a "type of types").
data Optionality = Opt | Req

-- Because the Opt and Req *types* are uninhabited, we need something
-- else we can pass as the first argument to our function. Note that
-- the separate type signature for the data type is called
-- "stand-alone kind signature"; this is relatively new syntax but
-- makes things a lot clearer.
type OptionalitySingleton :: Optionality -> Type
data OptionalitySingleton a where
  SingletonForOpt :: OptionalitySingleton Opt
  SingletonForReq :: OptionalitySingleton Req

-- Again I've provided a stand-alone kind signature to make it clear
-- what kinds of type MaybeWrapper works with.
type MaybeWrapper :: Optionality -> Type -> Type
type family MaybeWrapper o v where
  MaybeWrapper Opt v = Maybe v
  MaybeWrapper Req v = v

-- Finally, f itself is almost trivial
f :: OptionalitySingleton a -> v -> MaybeWrapper a v
f SingletonForOpt vv = Just vv
f SingletonForReq vv = vv

(Note that I've used annoyingly long names for clarity of the example; normally when applying this pattern people use much shorter names; Sing or S as prefix/suffix are quite common)

You're probably wondering why you couldn't just use Opt and Req as the first argument to f; why did I mess around with the whole separate OptionalitySingleton type? But if we used the value level Opt and Req then the type of that paramter would have to be just Optionality, the type of f would have to look like this:

f :: Optionality -> v -> MaybeWrapper a v

Here the a in MaybeWrapper a v is totally unrelated to the Optionality first parameter, so we don't learn anything about a by pattern matching on the Optionality value. And there's no variable in the type Optionality, so there's nothing we can connect to a.

Whereas the type-level Opt and Req don't have any values at all (only types in the kind Type have values; type-level Opt and Req are in the kind Optionality instead), so there's nothing we could pass to f. Even if we could, they're different types, so there are no patterns that would be valid for both of them that we could use when we don't know what the type parameter is yet.

So instead we have to define a separate type like OptionalitySingleton (using the where syntax to define a type is a feature known as GADT or Generalised Algebraic Data Type syntax, if you haven't seen it and want to google for more information). This pattern takes a type parameter and then defines the type so that there is only a single possible constructor for each value of the type parameter (hence the term "singleton", which is completely unrelated to the term singleton in object-oriented programming). This means that pattern matching on the constructors completely identifies what the type parameter must be, and there is special support built into the compiler for making use of the evidence gained by pattern matching on GADTs.

So f can just go ahead and pattern match on the OptionalitySingleton value and then use different return types in each branch. As above with the two eqT branches you still need to be explicit about what type you're matching in each branch. There's no way to use _ or otherwise and have a catch-all branch because we can still only write branches with positive evidence of type equality, we can't write a branch with usable evidence of type inequality. But now we have limited it so that the only possible types are Opt and Req (or rather the only possible values are SingletonForOpt and SingletonForReq); the compiler will warn us (with -Wall) if we forget to handle all the cases (very useful when you later extend the Optionality to have a 3rd possibility and need to update every place you pattern match on it), and will in fact also warn us if we add another case in f (the compiler will notice that it must be redundant, as we've already matched everything that possibly could be matched).