Renamer hangs (because of -XInstanceSigs?)

changed weight to 5

added Tbug Trac import TypeInType labels

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?

Ah, I forgot.

You have to add ScopedTypeVariables, that should be enough.

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

changed the description

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

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

Great bug report. Patch coming

changed milestone to %8.6.1

changed weight to 10

assigned to @rae

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.

Trac metadata

Trac field	Value
Priority	normal → highest
Test case	- → polykinds/T14846

changed milestone to %8.4.2

changed weight to 5

Patch looks good to me.

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

Trac metadata

Trac field	Value
Priority	highest → normal

added 1 deleted label

removed 1 deleted label

closed

Merged to ghc-8.4.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

mentioned in issue #15141 (closed)

added InstanceSigs label

added Pnormal label

Renamer hangs (because of -XInstanceSigs?)

Child items ...

Activity