Opened 2 years ago

Last modified 11 months ago

#14164 new bug

GHC hangs on type family dependency

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.2.1
Keywords: InjectiveFamilies Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T14164
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# Language TypeOperators, DataKinds, PolyKinds, KindSignatures, TypeInType, GADTs, TypeFamilyDependencies #-}

import Data.Kind

type Cat a = a -> a -> Type

data SubList :: Cat [a] where
  SubNil :: SubList '[] '[]
  Keep   :: SubList xs ys -> SubList (x:xs) (x:ys)
  Drop   :: SubList xs ys -> SubList xs     (x:ys)

type family 
  UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where
  UpdateWith '[]    '[]    SubNil      = '[]
  UpdateWith (y:ys) '[]    SubNil      = y:ys
  -- UpdateWith '[]    (_:_)  (Keep _)    = '[]
  UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest
  -- UpdateWith ys     (x:xs) (Drop rest) = x:UpdateWith ys xs rest

seems to loop forever on the "Renamer/typechecker"

$ ghci -ignore-dot-ghci -v /tmp/u.hs 
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/  :? for help
Glasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC version 8.0.2

[...]

*** Parser [Main]:
!!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651 megabytes
*** Renamer/typechecker [Main]:

[hangs]

while

type family 
  UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where
  UpdateWith '[]    '[]    SubNil      = '[]
  UpdateWith (y:ys) '[]    SubNil      = y:ys
  UpdateWith '[]    (_:_)  (Keep _)    = '[]

immediately gives

$ ghc -ignore-dot-ghci /tmp/u.hs 
[1 of 1] Compiling Main             ( /tmp/u.hs, /tmp/u.o )

/tmp/u.hs:14:3: error:
    • Type family equations violate injectivity annotation:
        UpdateWith '[] '[] 'SubNil = '[] -- Defined at /tmp/u.hs:14:3
        forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
          UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
            -- Defined at /tmp/u.hs:16:3
    • In the equations for closed type family ‘UpdateWith’
      In the type family declaration for ‘UpdateWith’
   |
14 |   UpdateWith '[]    '[]    SubNil      = '[]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

/tmp/u.hs:16:3: error:
    • Type family equation violates injectivity annotation.
      Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’
      cannot be inferred from the right-hand side.
      Use -fprint-explicit-kinds to see the kind arguments
      In the type family equation:
        forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
          UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
            -- Defined at /tmp/u.hs:16:3
    • In the equations for closed type family ‘UpdateWith’
      In the type family declaration for ‘UpdateWith’
   |
16 |   UpdateWith '[]    (_:_)  (Keep _)    = '[]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Change History (18)

comment:1 Changed 2 years ago by Iceland_jack

(Does UpdateWith in any way (including with generalized injectivity #10832) makes sense as injective)

comment:2 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

I traced this down to a diverging call to tcUnifyTyWithTFs in FamInstEnvs.injectiveBranches. I don't know why it's diverging, but I do know that its arguments rhs1 and rhs2 are (according to pprTrace):

(rhs1) y_a1tT : UpdateWith ys2_a1tU xs_a1tV rest_a1tW
(rhs2) y_a1tR : ys_a1tS

comment:3 Changed 2 years ago by RyanGlScott

Keywords: InjectiveFamilies added

comment:4 Changed 18 months ago by RyanGlScott

Here's a somewhat smaller example that also loops at compile-time:

{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

data G (x :: a) = GNil | GCons (G x)

type family F (xs :: [a]) (g :: G (z :: a)) = (res :: [a]) | res -> a where
  F (x:xs) GNil         = x:xs
  F (x:xs) (GCons rest) = x:F xs rest

comment:5 Changed 17 months ago by Simon Peyton Jones <simonpj@…>

In d6216443/ghc:

Fix an infinite loop in niFixTCvSubst

Trac #14164 made GHC loop, a pretty serious error. It turned
out that Unify.niFixTCvSubst was looping forever, because we
had a substitution like
    a :-> ....(b :: (c :: d))....
    d :-> ...
We correctly recognised that d was free in the range of the
substitution, but then failed to apply it "deeeply enough"
to the range of the substiuttion, so d was /still/ free in
the range, and we kept on going.

Trac #9106 was caused by a similar problem, but alas my
fix to Trac #9106 was inadequate when the offending type
variable is more deeply buried.  Urk.

This time I think I've fixed it!  It's much more subtle
than I though, and it took most of a long train journey
to figure it out.  I wrote a long note to explain:
Note [Finding the substitution fixpoint]

comment:6 Changed 17 months ago by simonpj

Status: newmerge
Test Case: indexed-types/should_compile/T14164

Well that was harder than I thought. I've committed the change, but I'd welcome any review (eg Richard).

It fixes an outright bug, so I suggest merging to 8.6

comment:7 Changed 17 months ago by simonpj

PS: Thank you Iceland Jack and Ryan for an excellent bug report.

comment:8 Changed 17 months ago by goldfire

I've commented on the commit.

I think the fix is right, but I'm worried about other related scenarios. I suppose I'll repeat my worry here:

How do we know when performing a subst over an open type that we're not forgetting to subst in kinds? The in-scope set of a subst is always closed over kinds. But we need the (in-scope set) - (the subst domain), using set subtraction, to also be closed over kinds. Otherwise, we're substing a kind variable without substing the type variable, leading to problems like the ones here. So I propose adding this to the substitution invariants and checking it appropriately.

Thoughts?

comment:9 Changed 17 months ago by simonpj

Can you give an example?

One thing to remember: normal substitution is (carefully designed to be) one-shot. That is, it's fine to substitute a :-> [a], say. Even if they happen to have the same unique, we think of the range and the domain as coming from different address spaces.

comment:10 Changed 17 months ago by Simon Peyton Jones <simonpj@…>

In 83a7b1c/ghc:

Adjust comments (Trac #14164)

comment:11 Changed 17 months ago by goldfire

Suppose a :: k and we substitute [k |-> Type] in Proxy k a. We end up with Proxy Type a, but the k in a's kind is not substituted.

comment:12 Changed 17 months ago by simonpj

Ah I see. So the underlying invariant is

  • Applying a substitution S to a type t should result in a well-kinded type S(t).

What do we need for that to be true? Perhaps this? If a is in fv(t)\dom(S) then fv(kind(a)) is disjoint from dom(S)?

That is, if there is free variable in t that we aren't substituting, then we aren't substituting in its kind either.

comment:13 Changed 17 months ago by goldfire

Assuming the substitution and type t are both well-kinded, yes.

And I agree with your next sentence. But I'd like to divorce the invariant from the type t, because we can. I believe your sentence is implied by

(*) INVARIANT: If S is a substitution, then inscope(S)\dom(S) is closed over kinds.

This is something easy enough to check for.

comment:14 Changed 17 months ago by bgamari

Milestone: 8.6.1
Resolution: fixed
Status: mergeclosed

This is already present in 8.6.

comment:15 Changed 17 months ago by simonpj

Resolution: fixed
Status: closednew

Richard and I had a chat yesterday. He is going to

  • Write the invariant in comment:13, along with a Note to explain it (based on this ticket).
  • Add an ASSERT to check it.
  • Comment substTy and substCo, in the variable cases, to explain why we do not need to substitute in the kind of a type variable, or the type of a coercion variable.

Reopening just to track this.

Last edited 17 months ago by simonpj (previous) (diff)

comment:16 Changed 17 months ago by simonpj

Yikes! I've just rediscovered #13959 which is precisely the same territory.

comment:17 Changed 16 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:18 Changed 11 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.