Reputation: 4562
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.
Upvotes: 3
Views: 108
Reputation: 120751
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
Upvotes: 6
Reputation: 116174
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.
Upvotes: 2