Opened 4 months ago

Closed 3 months ago

#14846 closed bug (fixed)

Renamer hangs (because of -XInstanceSigs?)

Reported by: Iceland_jack Owned by: goldfire
Priority: normal Milestone: 8.4.2
Component: Compiler Version: 8.5
Keywords: InstanceSigs TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T14846
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

{-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}

import Data.Kind
import Data.Proxy

type Cat ob = ob -> ob -> Type

data Struct :: (k -> Constraint) -> Type where
  S :: Proxy (a::k) -> Struct (cls::k -> Constraint)

type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)

data AStruct :: Struct cls -> Type where
  AStruct :: cls a => AStruct (Structured a cls)

class StructI (structured::Struct (cls :: k -> Constraint)) where
  struct :: AStruct structured

instance (Structured xx cls ~ structured, cls xx) => StructI structured where
  struct :: AStruct (Structured xx cls)
  struct = AStruct

data Hom :: Cat k -> Cat (Struct cls) where

class Category (cat::Cat ob) where
  i :: StructI a => ríki a a

instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
  -- Commenting out this instance signature makes the issue go away
  i :: forall a. StructI a => Hom ríki a a
  i = case struct :: AStruct (Structured a cls) of

Running on 8.2.1 and 8.5.20180105 both loop until interrupted

$ ghci -ignore-dot-ghci 199.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 199.hs, interpreted )
^CInterrupted.
> 
>

Change History (10)

comment:1 Changed 4 months ago by RyanGlScott

I can't reproduce this with either version of GHC you give:

$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:29:8: error:
    • Couldn't match type ‘ríki1’ with ‘Hom ríki’
      ‘ríki1’ is a rigid type variable bound by
        the type signature for:
          i :: forall k2 (cls1 :: k2 -> Constraint) (a :: Struct
                                                            cls1) (ríki1 :: Struct cls1
                                                                            -> Struct cls1 -> *).
               StructI a =>
               ríki1 a a
        at Bug.hs:29:8-42
      Expected type: ríki1 a a
        Actual type: Hom ríki a a
    • When checking that instance signature for ‘i’
        is more general than its signature in the class
        Instance sig: forall (a :: Struct cls0). StructI a => Hom ríki a a
           Class sig: forall k (cls :: k -> Constraint) (a :: Struct
                                                                cls) (ríki :: Struct cls
                                                                              -> Struct cls -> *).
                      StructI a =>
                      ríki a a
      In the instance declaration for ‘Category (Hom ríki)’
   |
29 |   i :: forall a. StructI a => Hom ríki a a
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:30:12: error:
    • Could not deduce: cls1 a1 arising from a use of ‘struct’
      from the context: Category ríki
        bound by the instance declaration at Bug.hs:28:10-65
      or from: StructI a
        bound by the type signature for:
                   i :: forall (a :: Struct cls0). StructI a => Hom ríki a a
        at Bug.hs:29:8-42
    • In the expression: struct :: AStruct (Structured a cls)
      In the expression: case struct :: AStruct (Structured a cls) of
      In an equation for ‘i’:
          i = case struct :: AStruct (Structured a cls) of
   |
30 |   i = case struct :: AStruct (Structured a cls) of
   |            ^^^^^^

What am I missing?

comment:2 Changed 4 months ago by Iceland_jack

Ah, I forgot.

You have to add ScopedTypeVariables, that should be enough.

comment:3 Changed 4 months ago by RyanGlScott

Description: modified (diff)

Thanks. I've updated the original program to reflect this.

comment:4 Changed 4 months ago by RyanGlScott

Description: modified (diff)

comment:5 Changed 4 months ago by RyanGlScott

Actually, this program doesn't hang—it actually produces a stack overflow after a certain amount of time!

$ time ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
stack overflow: use +RTS -K<size> to increase it

real    0m18.986s
user    0m18.472s
sys     0m0.540s
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --version
The Glorious Glasgow Haskell Compilation System, version 8.5.20180221

Here's what this looks like in -ddump-tc-trace:

runStage interact with inerts {
  workitem   =  [WD] $dStructI_a1MK {0}:: StructI
                                            (Structured
                                               a_a1LU[sk:4]
                                               (cls_a1Li[ssk:2] |> {co_a1M2}
                                                                   ->_N <Constraint>_N)) (CDictCan)
addFunDepWork
  [WD] $dStructI_a1MK {0}:: StructI
                              (Structured
                                 a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N))
  arising from a use of ‘struct’ at Bug.hs:32:12-17
  False
  arising from the type signature for:
                 i :: forall (a :: Struct cls).
                      StructI a =>
                      Hom ríki_a1Lj[ssk:2] a a
  at Bug.hs:31:8-42
  True
  arising from a functional dependency between constraints:
    ‘StructI
       (Structured
          a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N))’
      arising from a use of ‘struct’ at Bug.hs:32:12-17
    ‘StructI a_a1LU[sk:4]’
      arising from the type signature for:
                     i :: forall (a :: Struct cls).
                          StructI a =>
                          Hom ríki_a1Lj[ssk:2] a a
      at Bug.hs:31:8-42
  at Bug.hs:32:12-17
  False
end stage interact with inerts }
runStage top-level reactions {
  workitem   =  [WD] $dStructI_a1MK {0}:: StructI
                                            (Structured
                                               a_a1LU[sk:4]
                                               (cls_a1Li[ssk:2] |> {co_a1M2}
                                                                   ->_N <Constraint>_N)) (CDictCan)
doTopReact
  [WD] $dStructI_a1MK {0}:: StructI
                              (Structured
                                 a_a1LU[sk:4]
                                 (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N)) (CDictCan)
*** Exception: stack overflow

comment:6 Changed 4 months ago by RyanGlScott

In case you're worried about that UndecidableInstances part, here's a version that doesn't use UndecidableInstances:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

type Cat ob = ob -> ob -> Type

data Struct :: (k -> Constraint) -> Type where
  S :: Proxy (a::k) -> Struct (cls::k -> Constraint)

type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)

data AStruct :: Struct cls -> Type where
  AStruct :: cls a => AStruct (Structured a cls)

class StructI xx (structured::Struct (cls :: k -> Constraint)) where
  struct :: AStruct structured

instance (Structured xx cls ~ structured, cls xx) => StructI xx structured where
  struct :: AStruct (Structured xx cls)
  struct = AStruct

data Hom :: Cat k -> Cat (Struct cls) where

class Category (cat::Cat ob) where
  i :: StructI xx a => ríki a a

instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
  i :: forall xx a. StructI xx a => Hom ríki a a
  i = case struct :: AStruct (Structured a cls) of

comment:7 Changed 4 months ago by simonpj

Great bug report. Patch coming

comment:8 Changed 4 months ago by simonpj

Milestone: 8.6.1
Owner: set to goldfire
Priority: normalhighest
Test Case: polykinds/T14846

Fixed by

commit e99fdf775540440c1c58dc5ade3c5984dc49246f
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Feb 26 17:44:55 2018 +0000

    Fix a nasty bug in the pure unifier
    
    The pure unifier was building an infinite type, through a defective
    occurs check.  So GHC went into an infinite loop.
    
    Reason: we were neglecting the 'kco' part of the type, which
    'unify_ty' maintains.  Yikes.
    
    The fix is easy.  I refactored a bit to make it harder to
    go wrong in future.


>---------------------------------------------------------------

e99fdf775540440c1c58dc5ade3c5984dc49246f
 compiler/types/Unify.hs                 | 59 ++++++++++++++++++---------------
 testsuite/tests/polykinds/T14846.hs     | 39 ++++++++++++++++++++++
 testsuite/tests/polykinds/T14846.stderr | 43 ++++++++++++++++++++++++
 testsuite/tests/polykinds/all.T         |  1 +
 4 files changed, 116 insertions(+), 26 deletions(-)

Richard, can you just check my work? I'll leave the ticket open, but assign to you.

comment:9 Changed 3 months ago by goldfire

Milestone: 8.6.18.4.2
Priority: highestnormal
Status: newmerge

Patch looks good to me.

This is a clear bug and shouldn't be hard to merge.

comment:10 Changed 3 months ago by bgamari

Resolution: fixed
Status: mergeclosed

Merged to ghc-8.4.

Note: See TracTickets for help on using tickets.