{-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances, TypeOperators, TypeFamilies, 
    GADTs, CPP, ConstraintKinds, ScopedTypeVariables, FlexibleContexts, 
    EmptyDataDecls, KindSignatures, Rank2Types, PolyKinds, 
    LiberalTypeSynonyms, OverlappingInstances #-} 

-- {-# LANGUAGE IncoherentInstances #-}

module Prelude.Type.Match where

import Prelude.Type.Families
import Prelude.Type.Integer

-- | Match 
-- 
-- Used by Case to match patterns.
-- 
-- Match +a ?b -c
-- Given a type a, match it with a pattern b, unifying the type variables.
-- If it matches, c is True, otherwise c is False.
-- 
-- >>> value (T :: Match (Just True) (Just x) p => T '(x, p)) :: (Bool, Bool)
-- (True, True)
-- 
-- Match is in a seperate module because I use IncoherentInstances to
-- match type variables.

class Match (a :: k) (b :: k) (p :: Bool) | a b -> p

instance (a ~ b, p ~ True) => Match a b p

instance a ~ b => Match (a :: ()) b True

instance Match Nothing (Just a) False
instance (nothing ~ Nothing, true ~ true) => Match Nothing nothing true
instance false ~ False => Match (Just a) Nothing false
instance (just_b ~ Just b, Match a b p) => Match (Just a) just_b p

instance Match True False False
instance (true ~ True, match ~ True) => Match True true match
instance Match False True False
instance (false ~ False, match ~ True) => Match False false match

instance Match LT EQ False
instance Match LT GT False
instance (lt ~ LT, match ~ True) => Match LT lt match
instance Match EQ LT False
instance Match EQ GT False
instance (eq ~ EQ, match ~ True) => Match EQ eq match
instance Match GT EQ False
instance Match GT LT False
instance (gt ~ GT, match ~ True) => Match GT gt match

instance Match (Left a) (Right b) False
instance Match (Right a) (Left b) False
instance (left_b ~ Left b, Match a b p) => Match (Left a) left_b p
instance (right_b ~ Right b, Match a b p) => Match (Right a) right_b p

instance (e_f ~ '(e, f), Match a e p, Match b f q, r ~ (p && q)) => Match '(a, b) e_f r
instance (e_f_g ~ '(e, f, g), Match a e p, Match b f q, Match c g r, (p && q) ~ s, (r && s) ~ t) => Match '(a, b, c) e_f_g t
instance (e_f_g_h ~ '(e, f, g, h), Match a e p, Match b f q, Match c g r, Match d h s, (p && q) ~ t, (r && s) ~ u, (t && u) ~ v)
          => Match '(a, b, c, d) e_f_g_h v

instance Match '[] (x ': xs) False
instance Match (x ': xs) '[] False
instance (nil ~ '[], true ~ True) => Match '[] nil true
instance (cons ~ (y ': ys),
          Match x y m,
          If m
             (Match xs ys p)
             (p ~ False)) 
     => Match (x ': xs) cons p

instance Match Ones (One j) False
instance Match Ones (Zero j) False
instance Match Ones Zeros False
instance Match Zeros Ones False
instance Match Zeros (One j) False
instance Match Zeros (Zero j) False
instance Match (One i) Ones False
instance Match (One i) Zeros False
instance Match (One i) (Zero j) False
instance Match (Zero i) Ones False
instance Match (Zero i) (One i) False
instance Match (Zero i) Zeros False
instance (ones ~ Ones, true ~ True) => Match Ones ones true
instance (zeros ~ Zeros, true ~ True) => Match Zeros zeros true
instance (one_j ~ (One j), Match i j p) => Match (One i) one_j p
instance (zero_j ~ (Zero j), Match i j p) => Match (Zero i) zero_j p