Unsafe entailment with Haskell constraints

Question

I'm playing around with the constraints package (for GHC Haskell). I have a type family for determining if a type-level list contains an element:

type family HasElem (x :: k) (xs :: [k]) where
  HasElem x '[] = False                                                                               
  HasElem x (x ': xs) = True                                                                          
  HasElem x (y ': xs) = HasElem x xs

This works, but one thing it doesn't give me is the knowledge that

HasElem x xs   entails   HasElem x (y ': xs)

since the type family isn't an inductive definition of the "is element of" statement (like you would have in agda). I'm pretty sure that, until GADTs are promotable to the type level, there is no way to express list membership with a data type.

So, I've used the constraints package to write this:

containerEntailsLarger :: Proxy x -> Proxy xs -> Proxy b -> (HasElem x xs ~ True) :- (HasElem x (b ': xs) ~ True)
containerEntailsLarger _ _ _ = unsafeCoerceConstraint

Spooky, but it works. I can pattern match on the entailment to get what I need. What I'm wondering is if it can ever cause a program to crash. It seems like it couldn't, since unsafeCoerceConstraint is defined as:

unsafeCoerceConstraint = unsafeCoerce refl

And in GHC, the type level is elided at runtime. I thought I'd check though, just to make sure that doing this is ok.

--- EDIT ---

Since no one has given an explanation yet, I thought I would expand the question a little. In the unsafe entailment I'm creating, I only expect a type family. If I did something that involved typeclass dictionaries instead like this:

badEntailment :: Proxy a -> (Show a) :- (Ord a)
badEntailment _ = unsafeCoerceConstraint

I assume that this would almost certainly be capable of causing a segfault. Is this true? and if so, what makes it different from the original?

--- EDIT 2 ---

I just wanted to provide a little background for why I am interested in this. One of my interests is making a usable encoding of relational algebra in Haskell. I think that no matter how you define functions to work on type-level lists, there will be obvious things that aren't proved correctly. For example, a constraint (for semijoin) that I've had before looked like this (this is from memory, so it might not be exact):

semijoin :: ( GetOverlap as bs ~ Overlap inAs inBoth inBs
            , HasElem x as, HasElem x (inAs ++ inBoth ++ inBs)) => ...

So, it should be obvious (to a person) that if I take union of two sets, that it contains an element x that was in as, but I'm not sure that it's possible the legitimately convince the constraint solver of this. So, that's my motivation for doing this trick. I create entailments to cheat the constraint solver, but I don't know if it's actually safe.

Answer 1

I don't know if this will suit your other needs, but it accomplishes this particular purpose. I'm not too good with type families myself, so it's not clear to me what your type family can actually be used for.

{-# LANGUAGE ...., UndecidableInstances #-}
type family Or (x :: Bool) (y :: Bool) :: Bool where
  Or 'True x = 'True
  Or x 'True = 'True
  Or x y = 'False

type family Is (x :: k) (y :: k) where
  Is x x = 'True
  Is x y = 'False

type family HasElem (x :: k) (xs :: [k]) :: Bool where
  HasElem x '[] = 'False
  HasElem x (y ': z) = Or (Is x y) (HasElem x z)

containerEntailsLarger :: proxy1 x -> proxy2 xs -> proxy3 b ->
                          (HasElem x xs ~ 'True) :- (HasElem x (b ': xs) ~ 'True)
containerEntailsLarger _p1 _p2 _p3 = Sub Dict

An approach using GADTs

I've been having trouble letting go of this problem. Here's a way to use a GADT to get good evidence while using type families and classes to get a good interface.

-- Lots of extensions; I don't think I use ScopedTypeVariables,
-- but I include it as a matter of principle to avoid getting
-- confused.
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}

-- Some natural numbers
data Nat = Z | S Nat deriving (Eq, Ord, Show)

-- Evidence that a type is in a list of types
data ElemG :: k -> [k] -> * where
  Here :: ElemG x (x ': xs)
  There :: ElemG x xs -> ElemG x (y ': xs)
deriving instance Show (ElemG x xs)

-- Take `ElemG` to the class level.
class ElemGC (x :: k) (xs :: [k]) where
  elemG :: proxy1 x -> proxy2 xs -> ElemG x xs

-- There doesn't seem to be a way to instantiate ElemGC
-- directly without overlap, but we can do it via another class.
instance ElemGC' n x xs => ElemGC x xs where
  elemG = elemG'

type family First (x :: k) (xs :: [k]) :: Nat where
  First x (x ': xs) = 'Z
  First x (y ': ys) = 'S (First x ys)

class First x xs ~ n => ElemGC' (n :: Nat) (x :: k) (xs :: [k]) where
  elemG' :: proxy1 x -> proxy2 xs -> ElemG x xs

instance ElemGC' 'Z x (x ': xs) where
  elemG' _p1 _p2 = Here

instance (ElemGC' n x ys, First x (y ': ys) ~ 'S n) => ElemGC' ('S n) x (y ': ys) where
  elemG' p1 _p2 = There (elemG' p1 Proxy)

This actually seems to work, at least in simple cases:

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Int, Char])
Here

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Int, Int])
There Here

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Integer, Int])
There (There Here)

This doesn't support the precise entailment you desire, but I believe the ElemGC' recursive case is probably the closest you can get with such an informative constraint, at least in GHC 7.10.