Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,391
    • Issues 4,391
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 376
    • Merge Requests 376
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13775

Closed
Open
Opened Jun 01, 2017 by fizruk@trac-fizruk

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)
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#13775