Elem.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes, TypeApplications, TypeInType, TypeOperators,
             ScopedTypeVariables, TypeFamilies, UndecidableInstances,
             GADTs, ConstraintKinds, AllowAmbiguousTypes #-}

module Elem where

import Data.Type.Equality
import Data.Kind
import Unsafe.Coerce

data Dict c where
  Dict :: c => Dict c

class Elem x xs
instance Elem x (x ': ys)
instance {-# INCOHERENT #-} Elem x xs => Elem x (y ': xs)

-- * The first instance matches only when `x ~ y`. If don't want to forego
-- parametricity, we can't inspect this.
--
-- * The second instance _always_ matches, which means that no matter what `y`
-- gets instantiated to, the resulting constructor will always be `There`. Since
-- resolving the instances depends on the instantiation of `x` and `y`, we need
-- an INCOHERENT pragma to tell GHC that we really are happy with the second one.
elemThere :: forall x xs y. Dict (Elem x xs) -> Dict (Elem x (y : xs))
elemThere Dict = Dict