-- |
-- Module      :  Data.Constraint.Trivial
-- Copyright   :  (c) 2014-2016 Justus Sagemüller
-- License     :  GPL v3 (see LICENSE)
-- Maintainer  :  (@) jsag $ hvl.no
--
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE Rank2Types              #-}
{-# LANGUAGE EmptyCase               #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE TypeInType              #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE AllowAmbiguousTypes     #-}

module Data.Constraint.Trivial (
          -- * Trivial classes
            Unconstrained0, Impossible0
          , Unconstrained, Impossible
          , Unconstrained2, Impossible2
          , Unconstrained3, Impossible3
          , Unconstrained4, Impossible4
          , Unconstrained5, Impossible5
          , Unconstrained6, Impossible6
          , Unconstrained7, Impossible7
          , Unconstrained8, Impossible8
          , Unconstrained9, Impossible9
          -- * Utility
          , Disallowed, nope
          ) where

import           GHC.TypeLits
import           GHC.Exts (Any, TYPE)

class Any => Bottom where
  no :: a
class (Bottom, TypeError ('Text "All instances of "
          ':<>: 'Text t
          ':<>: 'Text " are disallowed.")) => Disallowed t

-- | A term-level witness that the context contains a 'Disallowed' constraint, i.e.
--   one of the 'Impossible0', 'Impossible' ... constraints. In such a context, because
--   you are guaranteed that it can under no circumstances actually be invoked, you
--   are allowed to to anything whatsoever, even create a value of an uninhabited unlifted
--   type.
nope :: forall rep (a :: TYPE rep). Bottom => a
nope :: a
nope = case Any
forall a. Bottom => a
no of

-- | A constraint that is always/unconditionally fulfilled. This behaves the same
--   way as @()@, when appearing in a constraint-tuple, i.e. it does not change anything
--   about the constraints. It is thus the identity of the @(,)@ monoid in the constraint
--   kind.
class Unconstrained0
instance Unconstrained0
Unconstrained0

-- | A constraint that never is fulfilled, in other words it is guaranteed that something
--   whose context contains this constraint will never actually be invoked in a program.
class Disallowed "Impossible0" => Impossible0


-- | A parametric non-constraint. This can be used, for instance, when you have an
--   existential that contains endo-functions of any type of some specified constraint.
--
-- @
-- data GenEndo c where
--   GenEndo :: c a => (a -> a) -> GenEndo c
-- @
-- 
--   Then, you can have values like @GenEndo abs :: GenEndo Num@. It is also possible
--   to have @GenEndo id :: GenEndo Num@, but here the num constraint is not actually
--   required. So what to use as the @c@ argument? It should be a constraint on a type
--   which does not actually constrain the type.
-- 
-- @
-- idEndo :: GenEndo Unconstrained
-- idEndo = GenEndo id
-- @
class Unconstrained t
instance Unconstrained t


-- | This constraint can /never/ be fulfilled. One application in which this can be
--   useful is as a default for a class-associated constraint; this basically disables
--   any method with that constraint: so it can safely be left 'undefined'. We provide
--   the 'nope' method as a special form of 'undefined', which actually guarantees it
--   is safe through the type system. For instance, the old monad class with
--   its controversial 'fail' method could be changed to
--
-- @
-- class Applicative m => Monad m where
--   (return,(>>=)) :: ...
--   type FailableResult m :: * -> Constraint
--   type FailableResult m = Impossible  -- fail disabled by default
--   fail :: FailableResult m a => String -> m a
--   fail = nope
-- @
-- 
--   This would turn any use of fail in a “pure” monad (which does not actually
--   define 'fail') into a type error.
--   Meanwhile, “safe” uses of fail, such as in the IO monad, could be kept as-is,
--   by making the instance
--
-- @
-- instance Monad IO where
--   (return,(>>=)) = ...
--   type FailableResult m = Unconstrained
--   fail = throwErrow
-- @
-- 
--   Other instances could support the 'fail' method only selectively for particular
--   result types, again by picking a suitable @FailableResult@ constraint
--   (e.g. 'Monoid').
class Disallowed "Impossible" => Impossible t


-- | Like 'Unconstrained', but with kind signature @k -> k -> Constraint@
--   (two unconstrained types).
class Unconstrained2 t s
instance Unconstrained2 t s

class Disallowed "Impossible2" => Impossible2 t s


class Unconstrained3 t s r
instance Unconstrained3 t s r

class Disallowed "Impossible3" => Impossible3 t s r


class Unconstrained4 t s r q
instance Unconstrained4 t s r q

class Disallowed "Impossible4" => Impossible4 t s r q


class Unconstrained5 t s r q p
instance Unconstrained5 t s r q p

class Disallowed "Impossible5" => Impossible5 t s r q p


class Unconstrained6 t s r q p o
instance Unconstrained6 t s r q p o

class Disallowed "Impossible6" => Impossible6 t s r q p o


class Unconstrained7 t s r q p o n
instance Unconstrained7 t s r q p o n

class Disallowed "Impossible7" => Impossible7 t s r q p o n


class Unconstrained8 t s r q p o n m
instance Unconstrained8 t s r q p o n m

class Disallowed "Impossible8" => Impossible8 t s r q p o n m


class Unconstrained9 t s r q p o n m l
instance Unconstrained9 t s r q p o n m l

class Disallowed "Impossible9" => Impossible9 t s r q p o n m l