Opened 2 years ago
Last modified 9 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
comment:2 Changed 2 years ago by
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
Keywords: | InjectiveFamilies added |
---|
comment:4 Changed 16 months ago by
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:6 Changed 15 months ago by
Status: | new → merge |
---|---|
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:8 Changed 15 months ago by
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 15 months ago by
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:11 Changed 15 months ago by
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 15 months ago by
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 15 months ago by
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 15 months ago by
Milestone: | → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | merge → closed |
This is already present in 8.6.
comment:15 Changed 15 months ago by
Resolution: | fixed |
---|---|
Status: | closed → new |
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
andsubstCo
, 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.
comment:16 Changed 15 months ago by
Yikes! I've just rediscovered #13959 which is precisely the same territory.
comment:18 Changed 9 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
(Does
UpdateWith
in any way (including with generalized injectivity #10832) makes sense as injective)