Having to open quantified type class evidence manually?-CodePudding

Does one have to manually open the evidence like in prj' or is there a more direct way to guide the instance solver ?

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

module CatLib.SO.SO_TCMatchingDict where

class OneSide a where oneSide :: a

class (OneSide a {- , ManyOtherTC a -}) => TC a
instance (OneSide a {- , ManyOtherTC a -}) => TC a

class Other f where other :: forall a. f a

instance Other f => OneSide (f x) where oneSide = other


prj :: forall f a. (forall x. TC (f x)) => f a
prj = oneSide @(f a) -- Could not deduce (Other f) arising from a use of ‘oneSide’

prj' :: forall f g tag a b. (forall x. TC (f x)) => f a
prj' = case Dict :: Dict (TC (f a)) of
  Dict -> oneSide @(f a) -- that's ok

data Dict c = c => Dict

CodePudding user response：

How about

prj :: forall f a. (forall x. TC (f x)) => f a
prj = go
  where
    go :: TC (f a) => f a
    go = oneSide @(f a)

or, in one line:

prj :: forall f a. (forall x. TC (f x)) => f a
prj = oneSide :: TC (f a) => f a