CODEWITHSUNDEEP
haskelltype-families
Clinton
Clinton

Reputation: 23135

Equality constraints in type instances

Let's say I have the following:

type family TF a b

Can I write something like this

type instance TF Int t = (t ~ (x,y)) => (Int,x,y)

as a perhaps silly example.

This question is along the same theme as the accepted answer to this question: Haskell: Equality constraint in instance

I want to match the type instance even if I'm not sure the second argument is a pair then force the second argument to be a pair (with a resulting compile error if this is not successful).

Upvotes: 2

Views: 209

Answers (1)

Reid Barton
Reid Barton

Reputation: 15009

You might be able to do this in GHC 8.0 using the new TypeError feature, depending on what you mean by "force the second argument to be a pair". 

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

module Pair where

import GHC.TypeLits

type family Fst p where
  Fst (x, y) = x
  Fst _t = TypeError (Text "Fst: expected a pair, but got " :<>: ShowType _t)

type family Snd p where
  Snd (x, y) = y
  Snd _t = TypeError (Text "Snd: expected a pair, but got " :<>: ShowType _t)

type family TF a b
type instance TF Int t = (Int, Fst t, Snd t)

Now you should get a compile error if you try to apply TF Int to a non-tuple:

*Pair> let x = x in x :: TF Int Bool

<interactive>:9:1: error:
    • Fst: expected a pair, but got Bool
    • When checking the inferred type
        it :: (Int, (TypeError ...), (TypeError ...))

However, this doesn't really "force" the argument to be a pair any more than calling fromJust "forces" its argument to be of the form Just x. It is really programming with partial functions at the type level.

Well-formedness of type family applications is totally determined by the kind of the type family, and a pair (x, y) has the same kind * as, say, Bool does. You can't magically incur a constraint simply by writing down an application of a type family. If you want to get a constraint at the type level, you have to write it to the left side of =>.

In the linked question, CanFilter (b -> c) a is already a constraint, so it can imply b ~ c.

Upvotes: 4

Related Questions