Implicit Arguments and Type Families

Question

I've been experimenting with dependently typed programs using the Data.Singletons library, following the development of length-annotated vectors in the paper, "Dependently Typed Programming with Singletons," and I've run into the following problem.

This code, excluding the definition of the function indexI, typechecks in GHC 7.6.3 and works as expected in its absence:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons
import Data.Singletons.TH

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Eq

$(genSingletons [''Nat])

data FlipList :: * -> * -> Nat -> * where
    Cons :: ((a -> b) -> a -> b) -> FlipList a (a -> b) n -> FlipList a b (S n)
    Nil :: FlipList a b Z

type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Z = 'False
type instance Z :< (S n) = 'True
type instance (S m) :< (S n) = m :< n

type family PreMap a b (m :: Nat) :: *
type instance PreMap a b Z = a -> b
type instance PreMap a b (S n) = PreMap a (a -> b) n

type family BiPreMap a b (m :: Nat) :: *
type instance BiPreMap a b m = PreMap a b m -> PreMap a b m

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = f
index (SS sm) (Cons _ fl) = index sm fl

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

After including indexI, GHC produces two errors,

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

and,

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

The root of either error seems to be that the term withSing index has type FlipList a b n -> BiPreMap a b a0, and, without being able to deduce a0 ~ m, GHC is unable to prove BiPreMap a b m ~ BiPreMap a b a0. I know that type inference on type families lacks most of the conveniences we get when working with ADTS (injectivity, generativity, etc.), but my understanding of what the problem precisely is in this case, and how to circumvent it, is very limited. Is there some constraint I can specify that might clear it up?

Answer 1

What you should understand here is that there is in se nothing wrong with your code, it's just that GHC's type inference can't determine how it is type-safe. Note that by commenting out indexI, loading the code in GHC and asking for the type of withSing index:

*Main Data.Singletons> :t withSing index
  withSing index
    :: (SingI Nat a, (a :< n) ~ 'True) =>
       FlipList a1 b n -> PreMap a1 b a -> PreMap a1 b a

This means that GHC is able to type-check your code, and it even infers the same type as what you specified (up to alpha-equivalence). So why doesn't it type-check your code?

The problem is that your code doesn't explicitly say how the type parameters of withSing should be instantiated, specifically that type variable a should be instantiated to the m from your type signature. It is conceivable that a should be instantiated to something else (e.g. [m] or m -> m) in order for your implementation withSing index to have the type you specified. GHC has no way to determine that a should be instantiated to m, you get the errors that you get. Note that GHC will not try to guess this kind of instantiations and that is a good thing. We do not want the type-level language of GHC to degenerate into a Prolog interpreter ;). It is in my opinion a bit too close to that already.

This means that you have two options to solve your problem. The first solution was suggested by user2407038 above: use type annotations to tell GHC how the type parameter a of function withSing should be instantiated. Let me repeat his code here for reference:

indexI :: forall m n a b . ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing (index :: SNat m -> FlipList a b n -> BiPreMap a b m)

Note that you need the explicit forall syntax in the type signature to make sure that the m from the type signature is in scope in the implementation of indexI (look up the documentation on GHC's ScopedTypeVariables extension for more info).

Your other alternative is to change your code so that GHC can determine how to instantiate a by type inference. To understand this, consider that GHC is telling you that it cannot deduce PreMap a b m ~ PreMap a b a0. This means that GHC has inferenced withSing index to the type I showed you at the start of this answer and is trying to find type instantiations to determine how this inferred type is equal to the type you annotated. To do this, it tries to solve an equality constraint BiPreMap a b m ~ BiPreMap a b a0, which is simplified to a simpler constraint PreMap a b m ~ PreMap a b a0. However, that's where it gets stuck. Because type families like PreMap are not necessarily injective, it can't decide from this that m must be equal to a0. One way to solve this is to change BiPreMap into a data type or newtype. Unlike type families, data types and newtypes are injective in their arguments and GHC can then solve the constraints:

newtype BiPreMap a b m = BiPreMap { getBiPreMap :: PreMap a b m -> PreMap a b m }

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = BiPreMap f
index (SS sm) (Cons _ fl) = BiPreMap (getBiPreMap (index sm fl))

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

That's it, I hope this clarifies some of what is going on... Note that the type of "dependently-typed programming in Haskell" that you're trying to do is non-trivial in Haskell and you may encounter more of this kind of problems along the way. Very often, explicit type signatures will be the solution to weird type errors that you may encounter. Explicit type applications would also be useful, but I understand that support for them is still missing or in progress in GHC.