import Prelude hiding (all, flip, map, filter) u = undefined data R -- Red data G -- Green data B -- Blue data W -- White data Cube u f r b l d type CubeRed = Cube R R R R R R type CubeBlue = Cube B B B B B B type Cube1 = Cube B G W G B R type Cube2 = Cube W G B W R R type Cube3 = Cube G W R B R R type Cube4 = Cube B R G G W W data True data False type family And b1 b2 and :: b1 -> b2 -> And b1 b2 and = u type instance And True True = True type instance And True False= False type instance And False True = False type instance And False False= False data Nil data Cons x xs data x ::: xs infixr 5 ::: type family ListConcat l1 l2 listConcat :: l1 -> l2 -> ListConcat l1 l2 listConcat = u type instance ListConcat Nil l = l type instance ListConcat (x:::xs) ys = x:::(ListConcat xs ys) type family Apply f a apply :: f -> a -> Apply f a apply = u data Rotation data Twist data Flip type instance Apply Rotation (Cube u f r b l d) = Cube u r b l f d type instance Apply Twist (Cube u f r b l d) = Cube f r u l d b type instance Apply Flip (Cube u f r b l d) = Cube d l b r f u type family Map f xs map :: f -> xs -> Map f xs map = u type instance Map f Nil = Nil type instance Map f (x:::xs) = Apply f x ::: Map f xs type family Filter f xs filter :: f -> xs -> Filter f xs filter = u type instance Filter f Nil = Nil type instance Filter f (x:::xs) = AppendIf (Apply f x) x (Filter f xs) type family AppendIf b x ys type instance AppendIf True x ys = x ::: ys type instance AppendIf False x ys = ys type family MapAppend f xs mapAppend :: f -> xs -> MapAppend f xs mapAppend = u type instance MapAppend f Nil = Nil type instance MapAppend f (x:::xs) = ListConcat (x:::xs) (Map f (x:::xs)) type family MapAppend2 f xs mapAppend2 :: f -> xs -> MapAppend2 f xs mapAppend2 = u type instance MapAppend2 f Nil = Nil type instance MapAppend2 f (x:::xs) = ListConcat (x:::xs) (MapAppend f (Map f (x:::xs))) type family MapAppend3 f xs mapAppend3 :: f -> xs -> MapAppend3 f xs mapAppend3 = u type instance MapAppend3 f Nil = Nil type instance MapAppend3 f (x:::xs) = ListConcat xs (MapAppend2 f (Map f (x:::xs))) data Orientations type instance Apply Orientations c = MapAppend3 Rotation ( MapAppend2 Twist ( MapAppend Flip (c:::Nil))) type family NE x y ne :: x -> y -> NE x y ne = u type instance NE R R = False type instance NE R G = True type instance NE R B = True type instance NE R W = True type instance NE G R = True type instance NE G G = False type instance NE G B = True type instance NE G W = True type instance NE B R = True type instance NE B G = True type instance NE B B = False type instance NE B W = True type instance NE W R = True type instance NE W G = True type instance NE W B = True type instance NE W W = False type family All l all :: l -> All l all = u type instance All Nil = True type instance All (False ::: xs) = False type instance All (True ::: xs) = All xs type family Compatible c1 c2 compatible :: c1 -> c2 -> Compatible c1 c2 compatible = u type instance Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) = All (NE f1 f2 ::: NE r1 r2 ::: NE b1 b2 ::: NE l1 l2) type family Allowed c cs allowed :: c -> cs -> Allowed c cs allowed = u type instance Allowed c Nil = True type instance Allowed c (y ::: ys) = And (Compatible c y) (Allowed c ys) type family Solutions cs solutions :: cs -> Solutions cs solutions = u type instance Solutions Nil = (Nil ::: Nil) type instance Solutions (c ::: cs) = AllowedCombinations (Apply Orientations c) (Solutions cs) type family AllowedCombinations os sols type instance AllowedCombinations os Nil = Nil type instance AllowedCombinations os (s ::: sols) = ListConcat (AllowedCombinations os sols) (MatchingOrientations os s) type family MatchingOrientations os sol type instance MatchingOrientations Nil sol = Nil type instance MatchingOrientations (o ::: os) sol = AppendIf (Allowed o sol) (o:::sol) (MatchingOrientations os sol) type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil) solution = solutions (u::Cubes) -- Did all this and now I don't know how to reduce the type of solution in order to display it

-- There is unfortunately, no simple way to print the normalised type. -- In fact, GHC goes to great length to show types with as little -- normalisation as possible to users. (Especially for error messages, -- that usually makes them much easier to understand.) However, with -- type families, I think we really ought to have a ghci command to -- specifically request a normalised type. I'll put that on my -- TODO list! -- For the moment, you can of course try forcing normalisation by -- triggering type errors; eg -- > :t solution :: Int

-- There is unfortunately, no simple way to print the normalised type. -- In fact, GHC goes to great length to show types with as little -- normalisation as possible to users. (Especially for error messages, -- that usually makes them much easier to understand.) However, with -- type families, I think we really ought to have a ghci command to -- specifically request a normalised type. I'll put that on my -- TODO list! -- For the moment, you can of course try forcing normalisation by -- triggering type errors; eg -- > :t solution :: Int

`-- What about a flag, e.g. -fshow-normalized-types ?`