Could not deduce from the context

Question

I have this type class. But it cannot deduce that type returned from goal equals isGoal's first variable's type. How to fix this?

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
class Problem p where 
    type State p :: * 
    data Action p :: * 

    goal :: Eq (State p) => State p 
    goal = undefined 

    isGoal :: Eq (State p) => State p -> Bool 
    isGoal s = s == goal

Ended up doing this

class Problem p where 
    type State p :: * 
    data Action p :: * 

    goal :: p -> State p 
    goal = undefined 

    isGoal :: Eq (State p) => p -> State p -> Bool 
    isGoal p s = s == goal p

It would be nice if you'd present error messages in some other way. Screenshots from a Windows console, seriously... — leftaroundabout
It doesn't realize you're trying to use goal from the same instance. — melpomene
@leftaroundabout Copying and pasting from the Windows console is pretty annoying, I can understand preferring to take a screenshot. — Ørjan Johansen
@Ørjan Johansen well, it can't be more annoying than copying and pasting from a Windows-console screenshot! Question is, why use the Windows console in the first place? Apart from switching to a better OS entirely, there's also the option of WinGHCi. — leftaroundabout
The biggest problem with screenshots is that there's no guarantee that the image will always be hosted and available. Please copy and paste! — AJF

leftaroundabout leftaroundabout · Accepted Answer · 2015-07-19T13:25:49

The hint is right there in the error message:

N.B.: ‘State’ is a type function, and may not be injective

What this means: an injective function f is a function where from f(x) = f(y) it follows that x = y. Now, we're talking type-level here, so if State were injective, it would follow from State p ~ State q that p ~ q.

In s == goal, the compiler knows it needs to unify goal with s (because == always compares values of the same type), so there we have it:

s :: State p
goal :: State q
State p ~ State q

but because State is not injective, the compiler can't infer that p ~ q, i.e. that we're only talking about a single instance of the type class.

Why not? Well, you could come up with:

instance Problem Int where
  type State Int = Bool
  goal = True

instance Problem Double where
  type State Double = Bool
  goal = False

Now we have State Int ~ State Double. Yet obviously Int and Double aren't the same type, and they define goal in contradictory ways.

“How to fix this” – well, you need to redesign the class.

You can use
```
class Problem p where 
  data State p :: * 
```
In this case, State is injective, because every instantiation needs to be hard-baked into a single instance Problem.

If you need the ability to define the actual State types elsewhere, you need to give the compiler an explicit hint which p should be used for goal. The usual solution are proxies or – preferrable IMO – tagged values:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Tagged

class Problem p where 
  type State p :: * 

  goal :: Eq (State p) => Tagged p (State p)
  goal = Tagged undefined

  isGoal :: Eq (State p) => Tagged p (State p) -> Bool 
  isGoal = isGoalDef

isGoalDef :: forall p . Eq (State p) => Tagged p (State p) -> Bool 
isGoalDef (Tagged s) = s == g
    where (Tagged g) = goal :: Tagged p (State p)

Could not deduce from the context

1 Answers