Type families case split, confluent

Elem.hs

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

module Elem where

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

type family IsElem (x :: k) (xs :: [k]) :: Bool where
  IsElem x '[] = False
  IsElem x (x : _) = True
  IsElem x (_ : xs) = IsElem x xs

type family Elem x xs :: Constraint where
  Elem x xs = IsElem x xs ~ True

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

elemThere :: forall x xs y. Dict (Elem x xs) -> Dict (Elem x (y : xs))
elemThere Dict =
  -- Consider two cases:
  --
  -- x  ~ y, then @IsElem x (x : _) = True@ by definition
  -- x /~ y, then @IsElem x (_ : xs) = IsElem x xs@, and we have
  --              a proof for @IsElem x xs ~ True@ in scope
  --
  -- GHC cannot deduce this on its own because it does not perform a case split
  -- on @x ~ y@.
  --
  -- Another way to look at it is that we actually do not care which type family
  -- clause is used for reduction. Assume we reduced using both of them and
  -- emitted an equality constraint for coincidence overlap: this equality
  -- constraint is @True ~ IsElem x xs@ (the first clause equals the second),
  -- and it holds.

  case elemAxiom @x @(y : xs) @True of
    Refl -> Dict

elemAxiom :: forall x xs b. IsElem x xs :~: b
elemAxiom = unsafeCoerce Refl

The solution suggested by https://github.com/Lysxia (https://twitter.com/lysxia/status/963252584264892416) allows to remove unsafeCoerce:

type family IsElem (x :: k) (xs :: [k]) :: Bool where
  IsElem x '[] = False
  IsElem y (x : xs) = IsElem y xs || y == x