Tying shoes with GADTs - Complete Code

Shoe.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Shoe where

data ShoeState = Off | Untied | On

data Shoes l r where
  PutOnL :: Shoes Off r -> Shoes Untied r 
  PutOnR :: Shoes l Off -> Shoes l Untied
  TieL   :: Shoes Untied r -> Shoes On r 
  TieR   :: Shoes l Untied -> Shoes l On
  OffLR  :: Shoes Off Off

type Method = Shoes Off Off -> Shoes On On

(>>>) = flip (.)

rllr :: Method
rllr = PutOnR >>> PutOnL >>> TieL >>> TieR

-- Doesn't type check:
-- don't :: Method
-- don't = TieR >>> TieL >>> PutOnR >>> PutOnL

describe :: Method -> IO ()
describe method = go (method OffLR) *> putStrLn "Done!"
  where
    go :: Shoes l r -> IO ()
    go OffLR = putStrLn "Alright."
    go (PutOnL x) = go x *> putStrLn "Put on the left shoe."
    go (PutOnR x) = go x *> putStrLn "Put on the right shoe."
    go (TieL x) = go x *> putStrLn "Tie the left shoe."
    go (TieR x) = go x *> putStrLn "Tie the right shoe."