Haskell's type families are strict -- they evaluate (or, try to evaluate) all of their arguments before they compute the result. When a type family doesn't have a matching equation, it is "stuck", and GHC just carries the applied type family around. This can be pretty confusing. If you want a type family to work on defined cases, and error otherwise, you must write a manual TypeError message: type family TurnOff (s :: Bool) where TurnOff True = False TurnOff _ = TypeError (Text "You tried to use TurnOff with False, but it can only be used with True.") Where TypError etc comes from `GHC.TypeLits` Matt Parsons On Fri, Jun 22, 2018 at 12:22 PM, Artem Pelenitsyn wrote:

Dear Benjamin,

I'm not sure I quite get your problem. My guess: you want a type-level guarantee that `turnOff'` function will only be applied to the terms of type `State True`, and so, you expect a compile-time error from `turnOff' off`. Am I get it right?

In your solution you seem to over engineer the solution. You try to relate type-level informaton (the value of of the type parameter `s` of `State`) to the term-level one (the value of the field stored in the `State` datatype). I think you'd better read how this task is solved with the technique known as singletons (https://cs.brynmawr.edu/~rae/ papers/2012/singletons/paper.pdf).

But I bet you don't need to solve that task to just address the problem at hand, if I understand the problem correctly. Please, tell me if the simpler solution below suits you: it doesn't use term-level (field of State) information at all.

{-# LANGUAGE DataKinds, TypeFamilies #-}

data State (s :: Bool) = State deriving Show

off :: State False off = State

type family TurnOff s where TurnOff True = False

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

bad = turnOff off -- <-- error: Couldn't match type ‘'False’ with ‘'True’

main = print bad https://ideone.com/boWN1q

-- Best, Artem

On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen wrote:

...

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'

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Jun 22, 2018, at 2:40 PM, Matt wrote:

Haskell's type families are strict

Not quite. Haskell's type families have no specific order of operation, at all. Here's a telling example:

data Nat = Zero | Succ Nat

type family Inf where Inf = Succ Inf

type family F a b where F True x = Int F False x = Char

type family Not a where Not True = False Not False = True

x :: F True Inf x = 5

y :: F False Inf y = 'a'

z :: F (Not False) Inf z = 42

Any attempt to evaluate Inf will cause GHC's evaluation stack to overflow and will result in an error. But x and y are accepted, because GHC can reduce F right away. z, on the other hand, causes this stack overflow, because GHC needs to reduce arguments in order to reduce F. GHC is not clever enough to notice that it needs to reduce only the first argument. This is silly, but it's unclear how to performantly do better. Richard