Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
    • Insights
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
    • Locked Files
  • Issues 3,623
    • Issues 3,623
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 204
    • Merge Requests 204
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Security & Compliance
    • Security & Compliance
    • Dependency List
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #10327

Closed
Open
Opened Apr 20, 2015 by Richard Eisenberg@rae
  • Report abuse
  • New issue
Report abuse New issue

Devise workaround for how infinite types prevent closed type family reduction

Suppose we have

data a :+: b

type family Inj x y where
  Inj a a = True
  Inj b (b :+: c) = False

When we try to reduce Inj f (f :+: g), it looks like we should just use the second equation. Instead, we fail to reduce. This is because GHC is worried about the possibility of the first equation firing, in the event that f ~ (f :+: g). This fact can happen only if f is infinitely large. On the surface, this seems impossible, but shenanigans in this area can cause unsafeCoerce. See #8162 (closed).

I don't see an easy way to fix this, but the fact that GHC can't cope (well) with this example tells me something is wrong. Here is one idea of how to proceed:

If we somehow ensure at reduction time that f is finite, we're OK. If we need finiteness in terms, we use deepseq. Can we do this in types? I tentatively say "yes".

Imagine the following type family:

type family Seq (x :: a) (y :: b) :: b

type instance Seq True  y = y
type instance Seq False y = y

To reduce, say, bSeq5, we'd need to know concretely what b is. We can then build Deepseq similarly to how deepseq at the term level works.

The closed type family mechanism could then detect cases like Inj, where the whole infinite-type thing is causing trouble. (I conjecture that detecting this is not hard, as there's a specific line in the Unify module that triggers in the worry-about-infinite-types case.) In the case of Inj, something like Inj f (f :+: g) would reduce to fDeepseqFalse. Note that the call to Seq wouldn't be written in the closed type family definition, but would be inserted during reduction as appropriate.

This solution is ugly. And it requires magic to define Seq in types (we need an instance for every type!) and weird magic in closed type family reduction. The definition of Deepseq might also benefit from being magical. It would be annoying to explain to users, but no more so than the current crazy story. In general, I don't like this idea much, but I do think it would work.

In any case, this ticket is mainly to serve as a placeholder for any future thoughts in this direction. It's quite annoying to have the specter of infinite types cripple otherwise-sensible closed type families.

Trac metadata
Trac field Value
Version 7.10.1
Type FeatureRequest
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Related issues

  • Discussion
  • Designs
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
3
Labels
feature request P::normal Trac import
Assign labels
  • View project labels
Reference: ghc/ghc#10327