custom-errors-example.hs

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE UndecidableInstances  #-}

module Test where

import GHC.TypeLits
import GHC.Generics
import Data.Kind
import Data.Proxy

newtype A = A String
  deriving Show

newtype B = B String
  deriving Show

data Sum
  = SumA A
  | SumB B
  deriving (Generic, Show)

-- inject (A "hello") :: Sum
-- >>> SumA (A "hello)
--
-- -----------------------------
--
-- inject "hello" :: Sum
--
-- <interactive>:10:1: error:
--     • Sum has no constructor containing [Char]
--     • In the expression: inject "hello" :: Sum
--       In an equation for ‘it’: it = inject "hello" :: Sum

class Has t sum where
  inject :: t -> sum

--------------v- need to check that the sum indeed contains the type, which is an
--                      additional traversal of `Rep sum that I don't know how to avoid
instance (ShowError sum t (Contains (Rep sum) t), Generic sum, GHas t (Rep sum)) => Has t sum where
  inject = to . ginject

type family ShowError (sum :: *) (t :: *) (contains :: Bool) :: Constraint where
  ShowError sum t 'False
    = TypeError ( 'ShowType sum
                ':<>: 'Text " has no constructor containing "
                ':<>: 'ShowType t)
  ShowError _ _ _ = ()







class GHas t (sum :: * -> *) where
  ginject :: t -> sum x

instance GHas t cs => GHas t (D1 meta cs) where
  ginject t = M1 (ginject t)

instance GHas t cs => GHas t (C1 meta cs) where
  ginject t = M1 (ginject t)

instance GHasSum t f g (Contains f t) => GHas t (f :+: g) where
  ginject = ginjectSum (Proxy :: Proxy (Contains f t))

type family Contains (rep :: * -> *) (t :: *) :: Bool where
  Contains (D1 _ c) t
    = Contains c t
  Contains (C1 _ c) t
    = Contains c t
  Contains (S1 _ (Rec0 t)) t
    = 'True
  Contains (f :+: g) t
    = Contains f t || Contains g t
  Contains _ t
    = 'False

type family a || b where
  'True || _ = 'True
  _     || x = x


class GHasSum t f g (which :: Bool) where
  ginjectSum :: proxy which -> t -> (f :+: g) x

instance GHas t f => GHasSum t f g 'True where
  ginjectSum _ t = L1 (ginject t)

instance GHas t g => GHasSum t f g 'False where
  ginjectSum _ t = R1 (ginject t)

instance GHas t (S1 meta (Rec0 t)) where
  ginject t = M1 (K1 t)