Opened 5 months ago

Closed 2 months ago

#13601 closed bug (fixed)

GHC errors but hangs

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.0.1
Keywords: TypeInType, LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_fail/T13601
Blocked By: Blocking:
Related Tickets: #13819 Differential Rev(s): Phab:D3794
Wiki Page:

Description

{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}

import GHC.Exts
import Prelude (Bool(True,False),Integer,Ordering,undefined)
import qualified Prelude
import Data.Kind

--------------------
-- class hierarchy

type family
  Rep (rep :: RuntimeRep) :: RuntimeRep where
  -- Rep IntRep         = IntRep
  -- Rep DoubleRep      = IntRep
  -- Rep PtrRepUnlifted = IntRep
  -- Rep PtrRepLifted   = PtrRepLifted

class Boolean (Logic a) => Eq (a :: TYPE rep) where
  type Logic (a :: TYPE rep) :: TYPE (Rep rep)
  (==) :: a -> a -> Logic a

class Eq a => POrd (a :: TYPE rep) where
  inf :: a -> a -> a

class POrd a => MinBound (a :: TYPE rep) where
  minBound :: () -> a

class POrd a => Lattice (a :: TYPE rep) where
  sup :: a -> a -> a

class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
  maxBound :: () -> a

class Bounded a => Complemented (a :: TYPE rep) where
  not :: a -> a

class Bounded a => Heyting (a :: TYPE rep) where
  infixr 3 ==>
  (==>) :: a -> a -> a

class (Complemented a, Heyting a) => Boolean a

(||) :: Boolean a => a -> a -> a
(||) = sup

(&&) :: Boolean a => a -> a -> a
(&&) = inf

hangs with

$ ghci a.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( a.hs, interpreted )

a.hs:18:16: error:  C-c C-cInterrupted.

Change History (10)

comment:1 Changed 5 months ago by Iceland_jack

I was running out the door when I submitted that, here is a more minimal example

{-# Language TypeFamilies, DataKinds, TypeInType #-}
-- {-# Language FlexibleContexts, UndecidableSuperClasses #-}

import GHC.Exts -- (TYPE, RuntimeRep)
import Data.Kind

type family
  Rep (rep :: RuntimeRep) :: RuntimeRep

class B (F a) => A (a :: TYPE rep) where
  type F (a :: TYPE rep) :: TYPE (Rep rep)

class A a => B a

It is fixed by uncommenting the final two pragmas and writing

class A a => B (a :: TYPE rep)

Alternatively, only commenting out import GHC.Exts (TYPE, RuntimeRep) gives us an ever-so-slightly different error

c.hs:10:16: error:
    • Expected kind
Last edited 5 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 5 months ago by Iceland_jack

Keywords: TypeInType LevityPolymorphism added

comment:3 Changed 5 months ago by simonpj

I know roughly what is happening here.

  • When checking kinds we call solveEqualities which immediately reports type errors
  • The offending kind-equality constraint in this case has a TypeEqOrigin whose uo_thing is built by checkExpectedKind.
  • That uo_thing is printed as part of the error message. Alas it contains a type (not a kind); and that type involves some knot-tied TyCons. Result: black hole.

The exact details are still hazy to me. The entire uo_thing stuff seems pretty grim.

comment:4 Changed 5 months ago by simonpj

I wondered about deferring the errors in solveEqualities by re-emitting them. Just jotting it down here; entirely untested.

+{-
+       ; emitConstraints final_wc
+       ; traceTc "End solveEqualities }" (ppr final_wc)
+       ; when (anyErrorsWC final_wc) failM
+       ; return result }
+-}
@@ -145,0 +153,8 @@ solveEqualities thing_inside
+anyErrorsWC :: WantedConstraints -> Bool
+anyErrorsWC (WC { wc_simple = wanteds, wc_insol = insols, wc_impl = implics })
+  =   anyBag is_err wanteds
+   || anyBag is_err insols
+   || anyBag (anyErrorsWC . ic_wanted) implics
+  where
+    is_err ct = trulyInsoluble ct
+

comment:5 Changed 5 months ago by goldfire

The uo_thing field was introduced in order to keep error messages reasonably stable during the TypeInType merge. Pre-TypeInType, kind errors reported what type had the kind that was involved in the error, and I wanted to keep this functionality post-TypeInType. That's the only reason the field exists. It was (and is) my hope to use uo_thing also for term-level error messages, as I think we can improve these through its use.

One of the grim aspects of uo_thing is that unifyType's type starts with Outputable a => Maybe a -> ... in order to use (possibly) something as the thing in the uo_thing field. But passing Nothing to unifyType causes ambiguity errors, because we can't know what a should be. So I have noThing :: Maybe (HsExpr Name); noThing = Nothing to resolve the ambiguity. I've been meaning to clean this up.

Another missed opportunity after TypeInType is to use TcTyCon more fully. Type-checking can produce TcTyCons instead of TyCons, with the latter rewriting to the former only during the final zonk. This would mean that the type-checking knot needs to cover only zonking, instead of type-checking. That would surely fix this bug.

In more direct response to comment:4, I'm dubious. If solveEqualities fails, then there is something ill-kinded lurking about, and I'm worried that some failIfErrsM and such won't fire, causing chaos. It may be possible to rein in the chaos, but I don't think it will be an easy win.

comment:6 Changed 2 months ago by RyanGlScott

This appears to be fixed in GHC HEAD. I need to figure out which commit did the deed.

comment:7 Changed 2 months ago by RyanGlScott

This was fixed in c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 (Fix #13819 by refactoring TypeEqOrigin.uo_thing). TODO Add a regression test.

comment:8 Changed 2 months ago by RyanGlScott

Differential Rev(s): Phab:D3794
Status: newpatch

comment:9 Changed 2 months ago by Ryan Scott <ryan.gl.scott@…>

In 424ecadb/ghc:

Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794

comment:10 Changed 2 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: dependent/should_fail/T13601
Note: See TracTickets for help on using tickets.