answer for https://haskell-jp.slack.com/archives/C5666B6BB/p1545201727030200

associative-law.hs

#!/bin/env stack
{-
  stack --resolver=lts-12.24 script --package extensible
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

import           Data.Extensible
import           Data.Extensible.HList (HList(..))
import           Data.Type.Equality

main :: IO ()
main = print $ happend3 (#x @== True <: nil) (#y @== True <: nil) (#z @== True <: nil)

-- 最初singletonsを使おうかと思ったけど，xs,ys,zs がSingIではないので，
-- 証明はできてもsingByProxyとかを使ってここへの繋ぎ込みができない
happend3 :: Record xs -> Record ys -> Record zs -> Record (xs ++ ys ++ zs)
happend3 xs ys zs = case listAssoc (toHList xs) (toHList ys) (toHList zs) of Refl -> xs `happend` ys `happend` zs

-- なので，Extensible内部で使ってるHListに一度変換してその上で結合則の証明を与える
listAssoc :: HList h xs -> HList h ys -> HList h zs -> xs ++ (ys ++ zs) :~: (xs ++ ys) ++ zs
listAssoc  HNil        ys zs = Refl
listAssoc (HCons x xs) ys zs = case listAssoc xs ys zs of Refl -> Refl