content: {-# OPTIONS_GHC -fdefer-type-errors #-}
  -- {-# OPTIONS_GHC -w #-}
  {-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
  
  module TypeSpec where
  
  import Test.Hspec
  import GHC.TypeLits
  import Control.Exception (evaluate)
  import Data.Proxy
  import Test.ShouldNotTypecheck (shouldNotTypecheck)
  import TestUtils
  
  import Mezzo.Model.Types
  import Mezzo.Model.Prim
  import Mezzo.Model.Harmony
  
  typeSpec :: Spec
  typeSpec =
      describe "Mezzo.Model.Types" $ do
          describe "Harmonic types" $ do
              it "should convert roots to pitches" $ do
                  shouldTypecheck rootToPitch
                  shouldNotTypecheck rootToPitchInv
              it "should sharpen roots" $ do
                  shouldTypecheck sharpen
                  shouldNotTypecheck sharpenInv
              it "should flatten roots" $ do
                  shouldTypecheck flatten
                  shouldNotTypecheck flattenInv
              it "should make intervals" $ do
                  shouldTypecheck makeInterval
              it "should shift pitches by an interval" $
                  shouldTypecheck shift
          describe "Chords" $ do
              it "should convert chords to Music" $
                  shouldTypecheck fromChord
  
  rootToPitch ::
          ( (RootToPitch (PitchRoot (Pitch C Natural Oct3)) ~ (Pitch C Natural Oct3))
          , (RootToPitch (DegreeRoot (Key D Flat MinorMode) (Degree IV Natural Oct2)) ~ (Pitch F Sharp Oct2))
          ) => Bool
  rootToPitch = True
  
  rootToPitchInv :: Proxy (RootToPitch (DegreeRoot (Key D Flat MinorMode) (Degree IV Natural Oct2)))
                 -> Proxy (Pitch E Natural Oct2)
  rootToPitchInv = id
  
  sharpen :: ( (Sharpen (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch C Sharp Oct3))
             , (Sharpen (PitchRoot (Pitch E Natural Oct3))) ~ (PitchRoot (Pitch F Natural Oct3))
             , (Sharpen (PitchRoot (Pitch C Flat Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))
             , (Sharpen (PitchRoot (Pitch B Natural Oct3))) ~ (PitchRoot (Pitch C Natural Oct4))
             , (Sharpen (DegreeRoot (Key F Sharp MinorMode) (Degree VI Natural Oct3))) ~ (PitchRoot (Pitch D Sharp Oct4))
             , (Sharpen (DegreeRoot (Key E Sharp MajorMode) (Degree VII Natural Oct3))) ~ (PitchRoot (Pitch F Natural Oct4))
             ) => Bool
  sharpen = True
  
  sharpenInv :: Proxy '(Sharpen (PitchRoot (Pitch B Flat Oct5)), Sharpen (DegreeRoot (Key C Flat MajorMode) (Degree IV Natural Oct3)))
             -> Proxy '(PitchRoot (Pitch C Flat Oct6), PitchRoot (Pitch F Natural Oct3))
  sharpenInv = id
  
  flatten :: ( (Flatten (PitchRoot (Pitch D Natural Oct3))) ~ (PitchRoot (Pitch D Flat Oct3))
             , (Flatten (PitchRoot (Pitch F Natural Oct3))) ~ (PitchRoot (Pitch E Natural Oct3))
             , (Flatten (PitchRoot (Pitch C Sharp Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))
             , (Flatten (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch B Natural Oct2))
             , (Flatten (DegreeRoot (Key F Sharp MinorMode) (Degree VI Natural Oct3))) ~ (PitchRoot (Pitch D Flat Oct4))
             , (Flatten (DegreeRoot (Key E Sharp MajorMode) (Degree VII Natural Oct3))) ~ (PitchRoot (Pitch E Flat Oct4))
             ) => Bool
  flatten = True
  
  flattenInv :: Proxy '(Flatten (PitchRoot (Pitch C Sharp Oct5)), Flatten (DegreeRoot (Key C Flat MajorMode) (Degree V Natural Oct3)))
             -> Proxy '(PitchRoot (Pitch B Sharp Oct4), PitchRoot (Pitch E Natural Oct3))
  flattenInv = id
  
  makeInterval ::
              ( (MakeInterval (Pitch C Natural Oct3) (Pitch E Natural Oct3)) ~ (Interval Maj Third)
              , (MakeInterval (Pitch E Natural Oct3) (Pitch C Natural Oct3)) ~ (Interval Maj Third)
              , (MakeInterval (Pitch C Natural Oct3) (Pitch B Flat Oct3)) ~ (Interval Min Seventh)
              , (MakeInterval (Pitch E Sharp Oct3) (Pitch E Sharp Oct3)) ~ (Interval Perf Unison)
              , (MakeInterval (Pitch E Natural Oct3) (Pitch F Flat Oct3)) ~ (Interval Dim Second)
              , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct3)) ~ (Interval Min Second)
              , (MakeInterval (Pitch F Sharp Oct3) (Pitch G Flat Oct3)) ~ (Interval Dim Second)
              , (MakeInterval (Pitch C Natural Oct3) (Pitch C Natural Oct4)) ~ (Interval Perf Octave)
              , (MakeInterval (Pitch E Flat Oct3) (Pitch F Flat Oct4)) ~ Compound
              , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct4)) ~ (Interval Maj Seventh)
              , (MakeInterval (Pitch C Natural Oct3) (Pitch F Sharp Oct3)) ~ (Interval Aug Fourth)
              , (MakeInterval (Pitch C Natural Oct3) (Pitch G Flat Oct3)) ~ (Interval Dim Fifth)
              , (MakeInterval (Pitch D Natural Oct3) (Pitch B Flat Oct3)) ~ (Interval Min Sixth)
              -- , (MakeInterval (Pitch D Natural Oct3) (Pitch A Sharp Oct3)) ~ (Interval Aug Fifth)
              , (MakeInterval (Pitch F Sharp Oct3) (Pitch A Natural Oct3)) ~ (Interval Min Third)
              -- , (MakeInterval (Pitch G Flat Oct3) (Pitch A Natural Oct3)) ~ (Interval Aug Second)
              , (MakeInterval (Pitch C Sharp Oct3) (Pitch B Natural Oct3)) ~ (Interval Min Seventh)
              -- , (MakeInterval (Pitch D Flat Oct3) (Pitch B Natural Oct3)) ~ (Interval Aug Sixth)
              -- , (MakeInterval (Pitch B Natural Oct3) (Pitch D Flat Oct3)) ~ (Interval Aug Sixth)
              -- , (MakeInterval (Pitch C Sharp Oct3) (Pitch C Flat Oct4)) ~ (Interval Dim Octave)
              , (MakeInterval (Pitch G Sharp Oct3) (Pitch E Natural Oct4)) ~ (Interval Min Sixth)
              -- , (MakeInterval (Pitch A Flat Oct3) (Pitch E Natural Oct4)) ~ (Interval Aug Fifth)
              , (MakeInterval (Pitch A Flat Oct3) (Pitch F Flat Oct4)) ~ (Interval Min Sixth)
              ) => Bool
  makeInterval = True
  
  shift ::
              ( (RaiseBy (Pitch C Natural Oct3) (Interval Maj Third) ~ (Pitch E Natural Oct3))
              , (LowerBy (Pitch E Natural Oct3) (Interval Maj Third)) ~ (Pitch C Natural Oct3)
              , (RaiseBy (Pitch C Natural Oct3) (Interval Min Seventh)) ~ (Pitch B Flat Oct3)
              , (RaiseBy (Pitch E Sharp Oct3) (Interval Perf Unison)) ~ (Pitch E Sharp Oct3)
              , (RaiseBy (Pitch E Natural Oct3) (Interval Min Second)) ~ (Pitch F Natural Oct3)
              , (LowerBy (Pitch F Natural Oct3) (Interval Min Second)) ~ (Pitch E Natural Oct3)
              , (RaiseBy (Pitch C Natural Oct3) (Interval Perf Octave)) ~ (Pitch C Natural Oct4)
              , (LowerBy (Pitch C Natural Oct4) (Interval Perf Octave)) ~ (Pitch C Natural Oct3)
              , (RaiseBy (Pitch E Sharp Oct3) (Interval Maj Seventh)) ~ (Pitch E Natural Oct4)
              , (RaiseBy (Pitch C Natural Oct3) (Interval Aug Fourth)) ~ (Pitch F Sharp Oct3)
              , (LowerBy (Pitch F Natural Oct4) (Interval Aug Fourth)) ~ (Pitch B Natural Oct3)
              , (RaiseBy (Pitch C Natural Oct3) (Interval Dim Fifth)) ~ (Pitch G Flat Oct3)
              , (LowerBy (Pitch F Natural Oct4) (Interval Dim Fifth)) ~ (Pitch B Natural Oct3)
              ) => Bool
  shift = True
  
  
  fromChord ::
              ( (FromChord (Triad (PitchRoot (Pitch C Natural Oct4)) MajTriad Inv0) 8)
                  ~ ( Pitch G Natural Oct4 ** 8 :- End
                  :-- Pitch E Natural Oct4 ** 8 :- End
                  :-- Pitch C Natural Oct4 ** 8 :- End :-- None)
              , (FromChord (Triad (PitchRoot (Pitch A Flat Oct4)) DimTriad Inv2) 8)
                  ~ ( Pitch B Natural Oct5 ** 8 :- End
                  :-- Pitch G Sharp Oct5 ** 8 :- End
                  :-- Pitch D Natural Oct5 ** 8 :- End :-- None)
              , (FromChord (Tetrad (PitchRoot (Pitch G Natural Oct4)) MajMinSeventh Inv0) 8)
                  ~ ( Pitch F Natural Oct5 ** 8 :- End
                  :-- Pitch D Natural Oct5 ** 8 :- End
                  :-- Pitch B Natural Oct4 ** 8 :- End
                  :-- Pitch G Natural Oct4 ** 8 :- End :-- None)
              , (FromChord (Tetrad (PitchRoot (Pitch B Sharp Oct3)) HalfDimSeventh Inv3) 8)
                  ~ ( Pitch F Sharp Oct5 ** 8 :- End
                  :-- Pitch D Sharp Oct5 ** 8 :- End
                  :-- Pitch C Natural Oct5 ** 8 :- End
                  :-- Pitch B Flat Oct4 ** 8 :- End :-- None)
              , (FromChord (Tetrad (PitchRoot (Pitch C Natural Oct4)) (DoubledT MajTriad) Inv0) 8)
                  ~ ( Pitch C Natural Oct5 ** 8 :- End
                  :-- Pitch G Natural Oct4 ** 8 :- End
                  :-- Pitch E Natural Oct4 ** 8 :- End
                  :-- Pitch C Natural Oct4 ** 8 :- End :-- None)
              , (FromChord (Tetrad (PitchRoot (Pitch C Sharp Oct4)) (DoubledT AugTriad) Inv1) 8)
                  ~ ( Pitch F Natural Oct5 ** 8 :- End
                  :-- Pitch C Sharp Oct5 ** 8 :- End
                  :-- Pitch A Natural Oct4 ** 8 :- End
                  :-- Pitch F Natural Oct4 ** 8 :- End :-- None)
              ) => Bool
  fromChord = True
  