maintaining type inference when repeating information in an instance head

M.hs

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module M where
import Prelude hiding ((.), id)

type Cat a b c = (SameKs a b c, C a b c)
class C a b c where
    (.) :: SameKs a b c => a -> b -> c

class ID a where id :: a

instance (a ~ a') => ID (a -> a') where id x = x
instance (ID x, ID y) => ID (x,y) where id = (id,id)

-- adding these SameK constraints ensures that ghc can assume
-- that if one parameter to the C class above is a tuple, then
-- all of them are tuples. Likewise if one is a function
class SameK' x y
instance (xy ~ (x,y))    => SameK' (a,b) xy
instance (xy ~ (x -> y)) => SameK' (a -> b) xy

type SameK x y = (SameK' x y, SameK' y x)
type SameKs a b c = (SameK a b, SameK b c)

instance (Cat f g fg, Cat f' g' fg') => C (f,f') (g,g') (fg,fg') where
    (f,f') . (g,g') = (f . g, f' . g')

instance (a ~ a', b ~ b', c ~ c') => C (b -> c) (a -> b') (a' -> c') where
    f . g = \x -> f (g x)


f = ((*2), (+ 1)) . ((*3), (/10) )

fid = f  . id
idf = id . f
{- ^ 

>>> :t f
f :: (Fractional y1, Num y) => (y -> y, y1 -> y1)

>>> :t fid
fid :: (Fractional y1, Num y) => (y -> y, y1 -> y1)

>>> :t idf
idf :: (Fractional y1, Num y) => (y -> y, y1 -> y1)

-}