[GHC] #14845: TypeInType, index by GADT witnessing constraint

23 Feb 2018


      #14845: TypeInType, index by GADT witnessing constraint
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Just wondering if it would ever make sense to allow or use constraints
 like this

 {{{#!hs
 {-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType,
 ConstraintKinds #-}

 import Data.Kind

 data Struct :: (k -> Constraint) -> (k -> Type) where
   S :: cls a => Struct cls a

 data Foo a where
   F :: Foo (S::Struct Eq a)
 }}}

 {{{
 $ ghci -ignore-dot-ghci /tmp/test.hs
 GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/test.hs, interpreted )

 /tmp/test.hs:9:13: error:
     • Illegal constraint in a type: cls0 a0
     • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
       In the type ‘Foo (S :: Struct Eq a)’
       In the definition of data constructor ‘F’
   |
 9 |   F :: Foo (S::Struct Eq a)
   |             ^
 Failed, no modules loaded.
 Prelude>
 }}}

 Please close the ticket if it doesn't

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14845
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler