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'