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,393
    • Issues 4,393
    • 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
  • #15577

Closed
Open
Opened Aug 29, 2018 by Ryan Scott@RyanGlScottMaintainer

TypeApplications-related infinite loop (GHC 8.6+ only)

The following program will loop infinitely when compiled on GHC 8.6 or HEAD:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

data family Sing :: forall k. k -> Type

class Generic1 (f :: k -> Type) where
  type Rep1 f :: k -> Type

class PGeneric1 (f :: k -> Type) where
  type From1 (z :: f a)      :: Rep1 f a
  type To1   (z :: Rep1 f a) :: f a

class SGeneric1 (f :: k -> Type) where
  sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
  sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)

class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
  sTof1 :: forall (a :: k) (z :: f a).      Sing z -> To1 (From1 z)        :~: z
  sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r

foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).
       VGeneric1 f
    => Sing r -> From1 (To1 r :: f a) :~: r
foo x
  | Refl <- sFot1 -- Uncommenting the line below makes it work again:
                  -- @Type
                  @f @a @r x
  = Refl

This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:35:20: error:
    • Expecting one more argument to ‘f’
      Expected a type, but ‘f’ has kind ‘* -> *’
    • In the type ‘f’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
   |
35 |                   @f @a @r x
   |                    ^

Bug.hs:35:23: error:
    • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
    • In the type ‘a’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                       ^

Bug.hs:35:26: error:
    • Couldn't match kind ‘* -> *’ with ‘*’
      When matching kinds
        f1 :: * -> *
        Rep1 f1 a1 :: *
      Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
    • In the type ‘r’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                          ^

Bug.hs:35:28: error:
    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
      When matching kinds
        a1 :: *
        'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
    • In the fourth argument of ‘sFot1’, namely ‘x’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                            ^

Bug.hs:36:5: error:
    • Could not deduce: From1 (To1 r1) ~ r1
      from the context: r0 ~ From1 (To1 r0)
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a pattern binding in
                      pattern guard for
                      an equation for ‘foo’
        at Bug.hs:33:5-8
      ‘r1’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).
                 VGeneric1 f1 =>
                 Sing r1 -> From1 (To1 r1) :~: r1
        at Bug.hs:(29,1)-(31,43)
      Expected type: From1 (To1 r1) :~: r1
        Actual type: r1 :~: r1
    • In the expression: Refl
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
36 |   = Refl
   |     ^^^^
Trac metadata
Trac field Value
Version 8.5
Type Bug
TypeOfFailure OtherFailure
Priority high
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
8.8.2
Milestone
8.8.2 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#15577