Why doesn't associated type synonym imply the constraint

user_7190191 0
Viewed 69

Why doesn't using an associated type synonym in a signature imply the corresponding constraint?

E.g. why doesn't the following compile:

{-# LANGUAGE TypeApplications, ScopedTypeVariables, TypeFamilies, AllowAmbiguousTypes #-}

class MyClass a where
  type AssociatedType a 
  bar :: Int

foo :: forall a. AssociatedType a -> Int
foo _ = bar @a

ghc 8.6.5 gives the following error:

error:
    * No instance for (MyClass a) arising from a use of `bar'
      Possible fix:
        add (MyClass a) to the context of
          the type signature for:
            foo :: forall a. AssociatedType a -> Int
    * In the expression: bar @a
      In an equation for `foo': foo _ = bar @a
  |
8 | foo _ = bar @a
  |         ^^^^^^

GHC documentation doesn't seem to mention this aspect.

type-families haskell
2 Answers

If it implied the constraint, then anybody using values of the associated value in any way whatsoever would need to have the constraint in scope. For example,

sort :: Ord a => [a] -> [a]

obviously knows nothing about MyClass, yet it should be possible to use it as sort :: [AssociatedType a] -> [AssociatedType a] provided that you have Ord (AssociatedType a) in the calling scope.

To get behaviour like the one you seem to be looking for, you want a wrapped constraint rather than an associated type. That can't be done with -XTypeFamilies, but it can be done with -XGADTs:

{-# LANGUAGE GADTs #-}

class MyClass a where
  bar :: Int

data MyClassWitness a where
  MyClassWitness :: MyClass a => MyClassWitness a

foo :: ∀ a. MyClassWitness a -> Int
foo MyClassWitness = bar @a

Instead of a self-rolled wrapper you can also use the one from the constraints library:

import Data.Constraint

foo :: ∀ a . Dict (MyClass a) -> Int
foo Dict = bar @a

Important in both cases is that you actually pattern-match on the GADT constructor, as only that actually brings the constraint into scope. This would not work:

foo :: ∀ a . Dict (MyClass a) -> Int
foo _ = bar @a
user_7459030

Because just using the type does not require the type constraint. For instance, this compiles:

foo :: forall a. AssociatedType a -> Int
foo _ = 42

At runtime, there is no need to pass a typeclass dictionary to this function, which is coherent with the lack of the constraint during type checking.

In your code, the constraint is needed because you are using bar, not because you are using the type.

user_32349590
Related