Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

file 43 lines (32 sloc) 1.281 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
module Data.Typewriter.TypeEq ( TypeEq(..), TypeNEq(..), (:/~)(..) )where

import Data.Typewriter.Core
import Data.Typewriter.Functions

-- | This is a modified version of Oleg's @TypeEq@. Note that @TypeCast@ is
-- no longer needed, as @~@ serves the same purpose.
class (TypeEq' () x y b) => TypeEq x y b where
    typeEq :: x -> y -> b
    maybeCast :: x -> Maybe y

instance (TypeEq' () x y b) => TypeEq x y b where
    typeEq _ _ = term
    maybeCast x = maybeCast' () x

class (TermProxy b) => TypeEq' q x y b | q x y -> b where
    maybeCast' :: q -> x -> Maybe y

instance (b ~ Yes) => TypeEq' () x x b where
    maybeCast' _ x = Just x

instance (b ~ No) => TypeEq' q x y b where
    maybeCast' _ _ = Nothing


class TypeNEq x y b where
    typeNEq :: x -> y -> b

instance (TermProxy b, TypeEq x y b', Not b' ~ b) => TypeNEq x y b where
    typeNEq x y = tNot $ typeEq x y


class (TypeNEq x y Yes) => x :/~ y
instance (TypeNEq x y Yes) => x :/~ y
Something went wrong with that request. Please try again.