Test.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}

module Main where


class Foo f where
    type Bar f :: *

    -- Attept 1: cannot be used in testfun because Bar is non-injective and Bar f0 is not known to equal Bar f
    -- qux :: Int -> Bar f -> Bar f

    -- Attempt 2: does not compile because Bar cannot be used in the same recursive group
    -- qux :: Int -> (a :: Bar f) -> a


data Xorb

instance Foo Xorb where
    type Bar Xorb = Int
    qux = (+)

testfun :: Foo f => Int -> Bar f -> IO ()
testfun v f = do r <- return $ qux v f
                 putStrLn "done"

main = testfun 3 (1 :: Bar Xorb)