Constraints in type family instances

Question

I'm exploring type families in Haskell, trying to establish the complexity of type-level functions I can define. I want to define a closed type-level version of mod, something like so:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits

type family Mod (m :: Nat) (n :: Nat) :: Nat where
  n <= m => Mod m n = Mod (m - n) n
  Mod m n = m

However, the compiler (GHC 7.10.2) rejects this, as the constraint in the first equation isn't permitted. How do guards at the value-level translate to the type level? Is this even possible in Haskell currently?

Answer 1

Not an answer (I don't think there even is one possible yet), but for the benefit of other people (like me) trying to retrace OPs steps in comments. The following compiles, but using it quickly results in a stack overflow.

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits
import Data.Type.Bool

type family Mod (m :: Nat) (n :: Nat) :: Nat where
  Mod m n = If (n <=? m) (Mod (m - n) n) m

The reason is that If itself is just a regular type family and the behavior of type-families is to start by expanding their type arguments (eager in a sense) before using those in the right hand side. The unfortunate result in this case is that Mod (m - n) n gets expanded even if n <=? m is false, hence the stack overflow.

For exactly the same reason, the logical operators in Data.Type.Bool do not short circuit. Given

type family Bottom :: Bool where Bottom = Bottom

We can see that False && Bottom and True || Bottom both hang.

EDIT

Just in case the OP is just interested in a type family with the required behavior (and not just the more general problem of having guards in type families) there is a way to express Mod in a way that terminates:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits

type Mod m n = Mod1 m n 0 m

type family Mod1 (m :: Nat) (n :: Nat) (c :: Nat) (acc :: Nat) :: Nat where
  Mod1 m n n acc = Mod1 m n 0 m
  Mod1 0 n c acc = acc
  Mod1 m n c acc = Mod1 (m - 1) n (c + 1) acc