Type Level Debugger

TypeLevelDebugger.hs

{-# LANGUAGE GADTs, UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, ScopedTypeVariables, OverlappingInstances, EmptyDataDecls #-}

data A a
data B a
data C a
data D a
data E a
data F a

type AToF =
  (A
  (B
  (C
  (D
  (E
  (F ()))))))

data Yes
data No
class TypeEqual x y b | x y -> b
instance TypeEqual a a Yes
instance No ~ b => TypeEqual x y b

class Tail aas as | aas -> as
instance Tail (a as) as
instance (r ~ ()) => Tail () r

class Contains' a b match r | a b match -> r
instance (Tail aas as, Contains as b r) => Contains' aas b No r
instance (r ~ Yes) => Contains' a b Yes r

class Contains as a r | as a -> r
instance (TypeEqual (a ()) b match, Contains' (a as) b match r) => Contains (a as) b r
instance Contains () b No

run :: (Contains as a yesOrNo) => as -> a -> yesOrNo
run = undefined
-- for i in {0..21}; do `ghc -fcontext-stack=${i} -i TypeLevelDebugger.hs -e "run (undefined :: AToF) (undefined :: F ())"`; done