'Having to open quantified type class evidence manually?

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


Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source