When working with FIFOs, it's sometimes desirable to using a blocking open, so that it will wait until a writer appears. base offers this in GHC.IO.Handle.FD.openFileBlocking
. However, that call is not interruptible. I've made a very simple singlethreaded program which is intended to blockingopen a FIFO repeatedly as its main loop, and which should shut down on ctrl+c, but in order to get this I had to hack up my own special open and read calls where the open call is marked interruptible
.
Unless it's a bad idea, set the c_safe_open
foreign call to interruptible
and make it deal properly with asynchronous exceptions. Otherwise, offer a new way to get an interruptible blocking open.
That last example is rejected early these days: you cannot have a type family in the conclusion of a quantified constraint.
Aha, fair enough. Has a better error message patch been merged? The error message I posted came from 8.6.5
I think the problem case below could be another symptom of this bug.
 Class.hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE TypeFamilies #}
module Class where
import Data.Kind (Type)
class ( Monad m, forall a . Ord (Family m a) ) => Class m where
type Family m :: Type > Type
 Bug.hs
module Bug where
import Class
import Data.Set (Set)
import qualified Data.Set as Set (insert)
bug :: (Class m) => Family m () > Set (Family m ()) > m (Set (Family m ()))
bug f s = pure (Set.insert f s)
Bug.hs:8:17: error:
• Could not deduce (Ord (Family m ()))
arising from a use of 'Set.insert'
from the context: Class m
bound by the type signature for:
bug :: forall (m :: * > *).
Class m =>
Family m () > Set (Family m ()) > m (Set (Family m ()))
at Bug.hs:7:177
• In the first argument of 'pure', namely '(Set.insert f s)'
In the expression: pure (Set.insert f s)
In an equation for 'bug': bug f s = pure (Set.insert f s)

8  bug f s = pure (Set.insert f s)
 ^^^^^^^^^^^^^^
Attached file 0002Fix11348handleinstancedependencies.2.patch
(download).
Fix candidate 2
Attached file 0002Fix11348handleinstancedependencies.patch
(download).
Fix candidate 1
Attached file 0002Fix11348collectmodulelocalfamilyinstances.patch
(download).
A potential fix.
Attached file character_kind.patch
(download).
An implementation of character kind
I see. So the necessary theoretical work just hasn't been done. I hope that eventually introG
can be accepted, but in the meantime, perhaps we could come up with a more helpful error message?
{# LANGUAGE GADTs #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
import Data.Proxy
 Defined to get the type forall x . 'D x
data D where
D :: a > D
type family F t :: D
 Will try to create values of this type through the type family
 F, i.e. G (F t)
data G (d :: D) where
G :: G ('D x)
 This is rejected because the type variable x in 'D x is ambiguous.
 But is it really? If there's an instance of F t then x is determined.
introG :: Proxy t > G (F t)
introG _ = G
 introG is welltyped if we add an equality constraint.
 Can GHC not figure this out without our help?
introG' :: forall t x . ( F t ~ 'D x ) => Proxy t > G (F t)
introG' _ = G
Here's the type error:
• Couldn't match type ‘F t’ with ‘'D x0’
Expected type: G (F t)
Actual type: G ('D x0)
The type variable ‘x0’ is ambiguous
• In the expression: G
In an equation for ‘introG’: introG _ = G
Trac field  Value 

Version  8.0.1 
Type  Bug 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler (Type checker) 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 
Replying to [ticket:11342#comment:131369 zyla]:
@alexvieth: Are you planning to work on this? If not, would you mind if I took your patch, implemented the changes mentioned above and posted it to Phab? (with appropriate credits of course)
Go for it!
Replying to [ticket:12088#comment:124925 simonpj]:
It is cool but it should have a separate ticket. Richard can you do that?
It's here: #11962
Simon, what do you think of my idea from comment 25?
Bottom line. Instead of getting in deeper, pull back. Do somthing that is simple to explain, predicatable, and simple to implement, even if it' a little less convenient.
The proposed phasing annotations might be convenient for ghc developers but they'd be inconvenient and surprising for ghc users. I appreciate that, at the term level, I don't need to worry about the order of my definitions. I'd like the same to be true at type level if possible, and I think it is possible. I'm just not sure if it will be simple to implement.
Sorry for the delay, new contract is keeping my occupied. ticket:12088#comment:123354 certainly shows a shortcoming in the patch for #11348 (closed). No sense reopening it though, this ticket can supersede it (its summary could use a revision for scope). Thanks for the wiki writeup mpickering. It's accurate and I have nothing to add right now. That section called "The Solution" is a tall order!
Replying to [ticket:12088#comment:123383 goldfire]:
This would then put illkinded equalities into the context. I think it would be awfully hard to avoid getting GHC to loop or do other silly things with a bad context. Perhaps you could squeeze this through, but I'm very skeptical.
Or am I misunderstanding something?
You're probably not misunderstanding. I'm just sounding off ideas and I'm no expert on GHC's type checker. Putting illkinded equalities into the context sounds irresponsible yes, but they'll all be of the form F k ~ l
for some open type family F
(or similar for higher arities). Does this fact help at all? Could you come up with a case where an illkinded equality of this form would wreak havoc?
How about a variation on that suggestion of mine? A kind of lazy evaluation for open type families in kinds. While type checking other declarations, rather than assuming the (possibly illkinded) equalities arising from open type families to be true, defer them until after all declarations are checked. Then we end up with a set of equalities featuring open type family constructors which must be solved using all open type family instances. So in the FieldCount
example from ticket:12088#comment:123354, repeated here for convenience:
{# LANGUAGE TypeInType, GADTs, TypeFamilies #}
import Data.Kind (Type)
data N = Z  S N
data Fin :: N > Type where
FZ :: Fin (S n)
FS :: Fin n > Fin (S n)
type family FieldCount (t :: Type) :: N
type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type
data T
type instance FieldCount T = S (S (S Z))
type instance FieldType T FZ = Int
type instance FieldType T (FS FZ) = Bool
type instance FieldType T (FS (FS FZ)) = String
The only declarations which give rise to a deferred kind equality are the FieldType
instances.
type instance FieldType T FZ = Int
yields S n0 ~ FieldCount T
type instance FieldType T (FS FZ) = Bool
yields S (S n1) ~ FieldCount T
type instance FieldType T (FS (FS FZ)) = String
yields S (S (S n2)) ~ FieldCount T
These don't stop type checking dead, they're just tucked away for later and type instance FieldCount T = S (S (S Z))
will eventually be checked (either before or after, we don't care) and available when those three equalities are solved. The program will therefore pass: n0 := (S (S Z))
, n1 := S Z
, n2 := Z
.
I'm still trying to grok the latest comments but in the meantime I want to offer an idea similar to this one:
Another idea: when we have a group of type instance decls, suppose we kind check them, but do not yet solve the kind equalities that arise; but add them to the instance environment anyway. Now solve all the kind equalities. In our example, we'd add both instances for Open1 and Open2 before trying to solve their kind equalities. Seems a bit scary somehow.
This doesn't seem scary to me. What if we don't even kind check them before adding their equalities to the environment? Just assume they're wellkinded while checking the other declarations. This way, we don't have to make sure the open type family instances come as early as possible in the order.
TyClGroup
s and the set of those instances (in source file order).TyClGroup
s, put all equalities arising from the open type family instances into the environment (assume for now that they're wellkinded).TyClGroup
s in order as usual.Maybe this is nonsense. Would it be possible to make and use a coercion axiom without kind checking the lhs and rhs types?
I'd like Richard E's opinion on all this
Me too. We also need to think about how a solution for this ticket would hold up under an implementation of #11962.
To me your example raises the question of whether it's even possible to figure out the dependencies. You probably believe that your "add extra edges" does so. But I still don't know exactly what those edges are. Maybe you could take a comment in this ticket to explain your algorithm precisely?
After a bit of thought I came up with a simple change to my last example:
 A.hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeInType #}
module A where
import Data.Kind
type family Open (t :: Type) :: Type
data family F (t :: Type) :: Open t > Type
 B.hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE GADTs #}
module B where
import Data.Kind
import A
data Q
type instance Open Q = Bool
data instance F Q r where
F0 :: F Q 'True
The difference is that the data family is defined in A.hs
and the family Closed
is no longer necessary, as the data family is enough to obscure the Open
dependency. B.hs
as given above will not pass with my approach, but swap the two instance declarations and it's fine.
So perhaps this small modification to my algorithm will work ...
The modification sounds good, but I share your worry and I think we're actually in for a bit more thinking.
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module A2 where
import Data.Kind
type family Open1 (t :: Type) :: Type
type family Open2 (t :: Type) (q :: Open1 t) :: Type
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE GADTs #}
module B where
import Data.Kind
import A2
type instance Open1 () = Bool
type instance Open2 () 'True = Char
The instance Open1 ()
needs to come before Open2 () 'True
to get that Open1 () ~ Bool
, but how are we to know this? Maybe we always check smaller instances (fewer parameters) before bigger ones?
Sorry to be slow... I'm on holiday.
No problem, enjoy it!
I've spent some more time studying this and now I'm even more convinced that we should stay with my solution. Take a look at these modules:
 A.hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE UndecidableInstances #}
module A where
import Data.Kind
type family Closed (t :: Type) :: Type where
Closed t = Open t
type family Open (t :: Type) :: Type
 B.hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE GADTs #}
module B where
import Data.Kind
import A
data Q
data family F (t :: Type) :: Closed t > Type
type instance Open Q = Bool
data instance F Q r where
F0 :: F Q 'True
The point is that type instance Open Q
must be checked before data instance F Q r
, even though we can't see this dependency, as it's hidden in A.hs
.
With Simon's suggestion, dependency analysis of B gives [data Q, data family F, type instance Open Q, data instance F Q r]
and then it's reordered to get [data Q, type instance Open Q, data family F, data instance F Q r]
(insert type instance Open Q
as early as possible, then do the same for data instance F Q r
). It's all good! But if we change the order of the definitions in the source file, we get a different result!
 B.hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE GADTs #}
module B where
import Data.Kind
import A
data family F (t :: Type) :: Closed t > Type
data Q
type instance Open Q = Bool
data instance F Q r where
F0 :: F Q 'True
Here we get [data family F t, data Q, type instance Open Q, data instance F Q r]
, and then we reorder it to [data family F t, data Q, type instance F Q r, type instance Open Q]
(first put type instance Open Q
as soon as possible, then put data instance F Q r
as soon as possible, which is right after data Q
). Checking type instance F Q r
causes a failure because we don't have type instance Open Q
yet.
The issue: this algorithm doesn't discover that type instance Open Q
can go before data family F t
. Whether it fails as above depends upon the order in which we choose to merge instance declarations into the TyClDecl
list, but in any case there will be a way to make it fail based on the order of declarations.
Taking some TyClDecl
order and then inserting the InstDecl
s without ever reordering the TyClDecl
s will not work. A more complicated algorithm is needed. The one I've implemented doesn't have this problem, thanks to the artificial dependency of data family F t
on type instance Open Q
.
I should also add that I don't think TyClGroup
should be changed to have only singleton InstDecl
groups. I'd say it's good that this type represents the actual dependency structure, regardless of whether it's valid according to the type checker. We'll let the type checker programs determine that after the groups are made, but having the renamer do this would be overextending the responsibilities of the renamer.
#12381 (closed) and #11348 (closed) were all about the order in which instance declarations are checked, but this case seems to be something different. Here there's no choice but to check these declarations in the order that they're written: the type family, then the class, then the instance of that class.
I suppose the type of D ()
should be (F a ~ Bool) => True
but as far as I know GHC can't handle such a thing.
We should figure out what fixed this
I believe it's #11348 (closed).
Alex suggests adding a potentially large number of extra edges, and thene doing standard SCC. But that seems a bit artifical, and I don't think it's easy to construct precisely the right extra edges.
Yes, there could be a lot of extra edges: at most the number of InstDecl
s multiplied by the number of TyClDecl
s. Computing them also requires a dfs for every TyClDecl
. Compiler performance isn't so great even without this change, so we should be careful.
I'm fairly certain that these are precisely the right extra edges.
 If
a > b
in the original graph, thena > b
in the augmented graph, because edges are never removed. The SCCs of the original are the same as in the augmented graph: an edge is added from
a
tob
only if there's no path fromb
toa
(on the graph including the other artificial edges).
Instances can't be mutually recursive, so singletons are what we need.
Do you mean that if an instance appears in a cyclic group, the program will definitely be rejected? If this is true, then your approach is viable, but we need to get the right error message. Perhaps the simplest way to do that is to continue using the existing mechanism brought about by tcTyClGroup
(which my patch does), but this would demand that we give the InstDecl
s in their cyclic groups should they arise.
Or what am I missing?
Nothing, you're right about this. The patch is now very small.
 a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ 881,7 +881,10 @@ tcTyVar mode name  Could be a tyvar, a tycon, or a datacon
; case thing of
ATyVar _ tv > return (mkTyVarTy tv, tyVarKind tv)
 ATcTyCon tc_tc > do { check_tc tc_tc
+ ATcTyCon tc_tc > do { unless
+ (isTypeLevel (mode_level mode))
+ (promotionErr name TyConPE)
+ ; check_tc tc_tc
; tc < get_loopy_tc name tc_tc
; handle_tyfams tc tc_tc }
 mkNakedTyConApp: see Note [Typechecking inside the knot]