On 18/06/15 17:19, Nicholls, Mark wrote:
data Z data S n
type family Sub a b type instance Sub a Z = a type instance Sub (S a) (S b) = Sub a b
I want this to be a type error!...but the above type family appears to not be partial…this IS defined….”Sub Z (S Z)” is a type! (I thought it wasn’t)
oneMinusTwo :: Sub Z (S Z) oneMinusTwo = undefined :: Sub (S Z) (S (S Z))
This is a slightly subtle point about type families. The type family application `Sub Z (S Z)` does not reduce, but neither is it an error. In this case, because Sub is an open type family, there is nothing to stop someone subsequently defining something like type instance Sub Z (S b) = Z in another module. Type families are functional relations, not functions in the FP sense. See also the discussion here, about the corresponding situation for a closed type family: https://ghc.haskell.org/trac/ghc/ticket/9636 Hope this helps, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/