{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-
This module contains solution for example from "Bidirectional type instances"
by Koen Pauwels, Georgios Karachalias, Michiel Derhaeg and Tom Schrijvers
(https://arxiv.org/pdf/1906.12242.pdf), using this package
-}
module Example1TH where
import Data.Kind (Constraint, Type)
import Control.Bidirectional ( Bidirectional, makeBidirectionalInstances, BidirectionalRec )
data Term :: Type -> Type where
Con :: a -> Term a
Tup :: Term b -> Term c -> Term (b, c)
{-
-- Fails to type check:
instance Show a => Show (Term a) where
show (Con x) = show x
show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
-}
{-
Some kind of solution using modern haskell without new extensions
-}
-- provide instances for which we want bidirectional constraints
makeBidirectionalInstances [d|
instance (Show b, Show c) => Show (b, c)
|]
-- then the following typechecks
instance BidirectionalRec Show a => Show (Term a) where
show (Con x) = show x
show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
-- of course we can also provide Bidirectional Show instance for Term, but it
-- isn't necessary, unless we want to have bidirectional constraint for it