How do you bind this type variable correctly?

I've been digging out some old code (and frankly regretting some design decisions) but I realized I could never get the final function to compile and I don't really understand why. I've got ScopedTypeVariables on which normally solves problems like this for me.

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, FlexibleContexts, RankNTypes #-}
{-# LANGUAGE DeriveTraversable, DerivingStrategies, ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Prelude hiding ((+), (*))
import Algebra
import Control.Lens.TH (makeLenses)
import Data.Semigroup (Semigroup, (<>))
import Data.Monoid (mempty, mappend)
import Data.Proxy (Proxy)
import Data.Function(on)
import qualified Data.IntMap as IM
import Control.Lens (IxValue, Index, Ixed(..), Traversal', Iso', view, review)

class (Ixed g) => Grid g where
    -- Stored x first, then y
    gridIso :: Iso' g (IM.IntMap (IM.IntMap (IxValue g)))
    storageVector :: (Index g) -> Vector2D Int

{-# INLINE gridIx #-}
gridIx :: forall g . (Grid g) => (Index g) -> Traversal' g (IxValue g)
gridIx v = gridIso . (ix x) . (ix y) 
   where (Vector2D x y) = storageVector v

instead I get this:

/mnt/c/Users/me/advent2018/src/Vector.hs:92:41: error:
    • Couldn't match expected type ‘Index g0’
                  with actual type ‘Index g’
      NB: ‘Index’ is a non-injective type family
      The type variable ‘g0’ is ambiguous
    • In the first argument of ‘storageVector’, namely ‘v’
      In the expression: storageVector v
      In a pattern binding: (Vector2D x y) = storageVector v
    • Relevant bindings include
        v :: Index g
          (bound at /mnt/c/Users/me/advent2018/src/Vector.hs:91:8)
        gridIx :: Index g -> Traversal' g (IxValue g)
          (bound at /mnt/c/Users/me/advent2018/src/Vector.hs:91:1)

Solution

What's happening here is that in order to call storageVector, the compiler has to choose an instance of Grid, but it can't.

Normally a parameter type would be enough to pick the instance, but in this case the parameter is of type Index g, and Index is a non-injective type family (as the error message states), which means that you can go from g to Index g, but you can't go back. In other words, there is no way to figure out what g is just by knowing Index g.

So the compiler can't choose a Grid instance and rejects the program.

To help the compiler with this, you can explicitly specify the type that should be used for instance lookup. To do that, use the TypeApplications extension:

    where (Vector2D x y) = storageVector @g v

This will tell the compiler that it should use instance Grid g for the same g.

Note that for this to work it is crucial to declare g with a forall keyword, which you're already doing.