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) |