How can a functional type dependency be used to obtain equality of type parameters?

Question

Consider the following code:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-} data St t = St { use_t :: t } class S st | s -> t where -- Nothing really newtype P s = P { unP :: forall b t. (S st) => St t -> (St t -> b) -- pok -> b } f :: (S st) => t -> P s ft = P $ \s pok -> pok s { use_t = t } 

The code seems far-fetched, but the idea is that the class S used to express that a parameter of type t is determined by a parameter of type S , so I don't need to add t as a type parameter for type P

The above code briefly gives the following error Could not deduce (t1 ~ t) from the context (S st) or from (S s t1) . This error message suggests that the compiler wants to use one or the other of these contexts, while I would hope that it would use both and wrap t1 ~ t with them.

I would appreciate any suggestions to get this working without adding t as the type parameter for input P

Answer 1

You cannot do this with the class as it is written. See Can I use an equality type layout from a functional dependency? . But you can do it with another class:

 class t ~ T s => S st where type T s :: * 

You need to define T for each instance, but at least it's not complicated. And you can provide a default definition of T , if there is one.

Answer 2

In the end, I solved the problem, because I also had another problem with my approach that could have been solved in this way not . This other problem was as follows:

 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-} data St tu = St { use_u :: u , use_t :: t } class Monad m => S smt | s -> t newtype P suma = P { unP :: forall b t. {-(Monad m,S smt) => -- Adding this causes problems with f -} St tu -> (a -> St tu -> mb) -- pok -> mb } w :: a -> P suma wx = P $ \s pok -> pok xs f :: (S smt) => P sum () f = P $ \s pok -> unP (w ()) s pok main = putStrLn "Hello world!" 

Adding type constraints to unP was essential for another solution, but it caused me problems with this. The t type parameter is used only in the St type, so I now solved the problem there using GADT. So the solution to my original problem was:

 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, GADTs #-} {-# LANGUAGE RecordWildCards #-} data St s where St :: (S st) => { use_t :: t } -> St s class S st | s -> t newtype P s = P { unP :: forall b. St s -> (St s -> b) -- pok -> b } -- Apparently the record update syntax is not fully implemented for GADTs, especially when using polymorphic fields. -- See https://www.reddit.com/r/haskell/comments/3r30pp/updating_polymorphic_records/?st=j5sno89f&sh=4ad675fb -- If you write your own update functions, trouble can be alleviated a bit using RecordWildCards . f :: (S st) => t -> P s -- ft = P $ \s pok -> pok s { use_t = t } ft = P $ \s pok -> pok $ update_use_t ts where update_use_t t = \(St {..}) -> St {use_t = t, ..} main = putStrLn "Hello world!" 

So the solution to my second problem was:

 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, GADTs #-} data St su where St :: (Monad m,S smt) => { use_u :: u , use_t :: t } -> St su class Monad m => S smt | s -> t newtype P suma = P { unP :: forall b. St su -> (a -> St su -> mb) -- pok -> mb } w :: a -> P suma wx = P $ \s pok -> pok xs f :: (S smt) => P sum () f = P $ \s pok -> unP (w ()) s pok main = putStrLn "Hello world!" 

Ultimately, this solution can still use the type equivalence constraints proposed by dfeuer.