How can I trigger a type error in Haskell?

Question

Let's suppose I have a type

data F a = A a | B

I implement the function f :: F a -> F a -> F a like this:

f (A x) B = A x
f B (A _) = B
f (A _) (A x) = A x

However no such thing as f B B it's logically impossible, so I want:

f B B = GENERATE_HASKELL_COMPILE_ERROR

which is not working of course. Omitting definition or using f B B = undefined is not a solution, because it generates runtime exception. I'd like to get a compile time type error.

The compiler has all the information, it should be able to deduce I made a logic error. If say I declare let z = f (f B (A 1)) B that should be an immediate compile time error and not some runtime exception which can hide in my code for years.

I have found some info about contracts but I do not know how to use them here, and I'm curious if there is any standard way to do this in Haskell.

---

EDIT: it's turned out, what I was trying to do is called dependent type which is not fully supported in Haskell (yet). Nevertheless it's possible to generate type error using index types and several extensions. David Young's solution seems to be more straightforward approach while Jon Purdy is using type operators creatively. I accept the first but I like both.

Answer 1

This is possible with some type tricks, but whether or not its worth it depends on what you're doing (incidentally, you should provide some more context so we can help determine how much type machinery seems like it is worth using).

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE ConstraintKinds #-}

import Data.Constraint

data AType
data BType

data F x y where
  A :: a -> F AType a
  B ::      F BType a

type family ValidCombo x y :: Constraint where
  ValidCombo BType ty2 = ty2 ~ AType
  ValidCombo ty1   ty2 = ()

f :: ValidCombo ty1 ty2 => F ty1 a -> F ty2 a -> F ty1 a
f (A x) B     = A x
f B     (A _) = B
f (A _) (A x) = A x

At compile time, it is both impossible to make a definition f B B = ... and it is impossible to try to call it like f B B. Your example let z = f (f B (A 1)) B will not type check (although more complex examples can run into issues).

The first thing that was done is I've added an extra argument to the F type constructor. This is a type index (there are no values of that type in anywhere, it is just a type level marker). I've created two different empty types (AType and BType) to use as phantom type arguments to F.

The type family ValidCombo acts as a function at the type level (notice that the definition is very similar to how a typical Haskell value-level function is defined, but with types instead of values). () is an empty constraint that never causes a type error (because an empty constraint is always, trivially, satisfied). At a type level, a ~ b constrains a and b to be the same type (~ is type-level equality) and will give an error if they are not the same type. It is roughly analogous to value-level code that looks like this (using your original F type), but at a type-level:

data Tag = ATag | BTag
  deriving Eq

getTag :: F a -> Tag
getTag (A _) = ATag
getTag B     = BTag

validCombo :: F a -> F a -> Bool
validCombo B tag2 = (getTag tag2) == ATag
validCombo _ _    = True

(this could be reduced, but I've left the "tag checking" and explicit equality in for a more clear comparison.)

You can go a little bit further with DataKinds to require the first type argument of F to either be AType or BType, but I don't want to add too much extra stuff (this is discussed a bit in the comments).

All that said, in many cases, the Maybe solution that @DirkyJerky has provided is the way to go (due to the added complexity of the type-level manipulations).

Sometimes this type-level technique is not even fully possible in Haskell at the moment (it potentially works on the example you've provided, but it depends on how it is going to be used), but you will need to provide more information for us to determine that.