absurd.hs

{-# LANGUAGE DataKinds, UndecidableInstances, ConstraintKinds, GADTs, FlexibleInstances, EmptyCase, LambdaCase #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

import GHC.TypeLits

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

class Impossible c where
  absurd :: Dict c -> a
  
instance e ~ TypeError (Text "Can't show functions") => Impossible e where
  absurd = \case

instance TypeError (Text "Can't show functions") => Eq (a -> b) where
  (==) = absurd Dict