Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,866
    • Issues 4,866
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 461
    • Merge requests 461
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19652
Closed
Open
Created Apr 05, 2021 by Richard Eisenberg@raeDeveloper

GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failure

Consider this mess:

{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
             StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
             TypeOperators #-}

module Bug where

import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )

type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
  Const '() x y = x

type Equals :: k1 -> k2 -> Type
type family Equals a b where
  Equals a a = Char
  Equals a b = Bool

type IsUnit :: () -> Type
data IsUnit u where
  ItIs :: IsUnit '()

f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
  => IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'

g = f ItIs

GHC fails (in the RHS of g) with an occurs-check, but it should succeed.

The problem is that we end up with

[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)

where we have already unified upsilon := '().

But GHC refuses to rewrite in kinds, so the Const never reduces, and we reject the program. Note that a solution exists, with alpha := Any @Type and beta := Any @Type |> sym (AxConst Type (Any @Type)).

Proposed solution:

The wanted above actually gets simplified to become

[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)

The co is easily solved. Then, when we get to w2, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that alpha is free in co and reorient, giving

[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)

which can be solved by unifying beta := alpha |> sym co. alpha will then remain unconstrained and will be zonked to Any.

The key new part is looking at the coercion when deciding whether to reorient.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking