Type family expansion is too lazy, allows accepting of ill-typed terms

I'm using GHC 8.0.2 and I've just witnessed a weird bug.

To reproduce a bug I use this type family, using TypeError (this is a minimal type family I could get to keep bug reproducible):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

type family Head xs where
  Head '[] = TypeError (Text "empty list")
  Head (x ': xs) = x

Then I go to GHCi, load this code and observe this:

>>> show (Proxy @ (Head '[]))
"Proxy"

This looks like a bug to me! I expect Head '[] to produce a type error. And indeed it does, if I ask differently:

>>> Proxy @ (Head '[])

<interactive>:9:1: error:
    • empty list
    • When checking the inferred type
        it :: Proxy (TypeError ...)

So far it looks like show somehow "lazily" evaluates it's argument type and that's why it's possible to show Proxy even when Proxy is ill-typed.

But if I expand Head '[] manually then it all works as expected again:

>>> show $ Proxy @ (TypeError (Text "error"))

<interactive>:13:8: error:
    • error
    • In the second argument of ‘($)’, namely
        ‘Proxy @(TypeError (Text "error"))’
      In the expression: show $ Proxy @(TypeError (Text "error"))
      In an equation for ‘it’:
          it = show $ Proxy @(TypeError (Text "error"))

You can remove TypeError from the original type family:

type family Head xs where
  Head (x ': xs) = x

And it gets even weirder:

>>> show (Proxy @ (Head '[]))
"Proxy"
>>> Proxy @ (Head '[])
Proxy

I did not test this with GHC 8.2.

I think this behaviour is not critical for me, but accepting ill-typed terms looks like a bad sign, especially for type-level-heavy programs.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	MacOS X
Architecture	x86_64 (amd64)