Re: [GHC] #2219: GADT match fails to refine type variable

[GHC]

#2219: GADT match fails to refine type variable
-+--
 Reporter:  dolio|  Owner:  chak   
 Type:  bug  | Status:  closed 
 Priority:  normal   |  Milestone:  6.10 branch
Component:  Compiler (Type checker)  |Version:  6.9
 Severity:  normal   | Resolution:  fixed  
 Keywords:  gadt type family | Difficulty:  Unknown
 Testcase:  T2219|   Architecture:  x86
   Os:  Linux|  
-+--
Changes (by chak):

  * testcase:  => T2219
  * status:  new => closed
  * resolution:  => fixed

Comment:

 Works with the new solver.

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #2219: GADT match fails to refine type variable

[GHC]

#2219: GADT match fails to refine type variable
-+--
 Reporter:  dolio|  Owner:  chak   
 Type:  bug  | Status:  new
 Priority:  normal   |  Milestone:  6.10 branch
Component:  Compiler (Type checker)  |Version:  6.9
 Severity:  normal   | Resolution: 
 Keywords:  gadt type family | Difficulty:  Unknown
 Testcase:   |   Architecture:  x86
   Os:  Linux|  
-+--
Changes (by igloo):

  * difficulty:  => Unknown
  * milestone:  => 6.10 branch

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #2219: GADT match fails to refine type variable

[GHC]

#2219: GADT match fails to refine type variable
+---
Reporter:  dolio|Owner:  chak 
Type:  bug  |   Status:  new  
Priority:  normal   |Milestone:   
   Component:  Compiler (Type checker)  |  Version:  6.9  
Severity:  normal   |   Resolution:   
Keywords:  gadt type family | Testcase:   
Architecture:  x86  |   Os:  Linux
+---
Changes (by chak):

  * owner:  => chak

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC] #2219: GADT match fails to refine type variable

[GHC]

#2219: GADT match fails to refine type variable
-+--
Reporter:  dolio |   Owner: 
Type:  bug   |  Status:  new
Priority:  normal|   Component:  Compiler (Type checker)
 Version:  6.9   |Severity:  normal 
Keywords:  gadt type family  |Testcase: 
Architecture:  x86   |  Os:  Linux  
-+--
 The following code is accepted by the type checker in 6.8.2, but is
 rejected by a HEAD build, 6.9.20080411:

 {{{
 {-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}

 data Zero
 data Succ a

 data FZ
 data FS fn

 data Fin n fn where
   FZ :: Fin (Succ n) FZ
   FS :: Fin n fn -> Fin (Succ n) (FS fn)

 data Nil
 data a ::: b

 type family Lookup ts fn :: *
 type instance Lookup (t ::: ts) FZ = t
 type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn

 data Tuple n ts where
   Nil   :: Tuple Zero Nil
   (:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)

 proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
 proj FZ  (v ::: _)  = v
 proj (FS fn) (_ ::: vs) = proj fn vs
 }}}

 The error in question is:

 {{{
 Bug.hs:25:16:
 Occurs check: cannot construct the infinite type:
   t = Lookup (t ::: ts) fn
 In the pattern: v ::: _
 In the definition of `proj': proj FZ (v ::: _) = v
 }}}

 Which seems to indicate that the pattern match against {{{FZ}}} in the
 first case is failing to refine the type variable {{{fn}}} to {{{FZ}}}.
 Reversing the order of the cases yields the same error, so either the
 match against FS is working correctly, or the type checker thinks that it
 can solve {{{Lookup (t ::: ts) fn ~ Lookup ts fn}}}.

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs