[Haskell-cafe] Type level seq

[Benjamin Franksen]

I have observed that type functions seem to be lazy. A type function
that is partial does not give me a type error when it is called with an
argument for which it is not defined.

Is there a 'seq' at the type level?

Here is my use case, simplified of course. Suppose we want to statically
track the state of a switch with a phantom type parameter:

> {-# LANGUAGE DataKinds, TypeFamilies #-}
>
> data State (s :: Bool) = State Bool deriving Show
>
> off :: State False
> off = State False

We want user code to be able to call the function 'turnOff' only if the
switch is currently on:

> turnOff :: State True -> State False
> turnOff (State True) = State False

This works fine:

*Main> turnOff off

<interactive>:1:9: error:
    ? Couldn't match type ?'False? with ?'True?
      Expected type: State 'True
        Actual type: State 'False

But now I want to abstract this pattern and write a (closed) type function

> type family TurnOff s where
>   TurnOff True = False

> turnOff' :: State x -> State (TurnOff x)
> turnOff' (State True) = State False

> bad = turnOff' off

*Main> :t bad
bad :: State (TurnOff 'False)
*Main> bad
*** Exception: TypeLevelSeq.lhs:37:3-37: Non-exhaustive patterns in
function turnOff'